Skip to content
This repository
Browse code

Make interactive HOL pay attention to PRE_INCLUDES variable.

Holmake was already doing the right thing here.

(PRE_INCLUDES allows users to re-use names for theories and modules
that the core system already used. However, this is not perfect in the
presence of preloaded theories that occur in standard heaps. In other
words, I doubt we will ever allow users to override "listTheory", for
example.)
  • Loading branch information...
commit ac146436031e6baf322b37f999cae02e55cce7e3 1 parent aa4e6aa
Michael Norrish authored August 08, 2012
18  std.prelude
@@ -167,23 +167,7 @@ in
167 167
   val _ = loadPath := tl (!loadPath)
168 168
 end;
169 169
 
170  
-val _ = if FileSys.access ("Holmakefile", [FileSys.A_READ]) then let
171  
-            open Holmake_types
172  
-            val (env, _, _) = ReadHMF.read "Holmakefile" base_environment
173  
-            fun envlist id =
174  
-                map dequote (tokenize (perform_substitution env [VREF id]))
175  
-            val hmake_includes = envlist "INCLUDES"
176  
-          in
177  
-            case hmake_includes of
178  
-              [] => ()
179  
-            | _ =>
180  
-              (print "[extending loadPath with Holmakefile INCLUDES variable]\n";
181  
-               loadPath := !loadPath @ hmake_includes)
182  
-          end handle e => (print "[bogus Holmakefile in current directory \
183  
-                                 \- ignoring it]\n";
184  
-                           TextIO.flushOut TextIO.stdErr;
185  
-                           ())
186  
-        else ()
  170
+use (OS.Path.concat (HOLDIR, OS.Path.concat("tools", "makefile-includes.ML")));
187 171
 
188 172
 structure HOL_Interactive : sig
189 173
   val toggle_quietdec : unit -> bool
19  tools-poly/prelude.ML
@@ -159,23 +159,7 @@ in
159 159
   app appthis ["internal_functions", "Holmake_types", "ReadHMF"]
160 160
 end;
161 161
 
162  
-val _ = if FileSys.access ("Holmakefile", [FileSys.A_READ]) then let
163  
-            open Holmake_types
164  
-            val (env, _, _) = ReadHMF.read "Holmakefile" base_environment
165  
-            fun envlist id =
166  
-                map dequote (tokenize (perform_substitution env [VREF id]))
167  
-            val hmake_includes = envlist "INCLUDES"
168  
-          in
169  
-            case hmake_includes of
170  
-              [] => ()
171  
-            | _ =>
172  
-              (print "[extending loadPath with Holmakefile INCLUDES variable]\n";
173  
-               loadPath := !loadPath @ hmake_includes)
174  
-          end handle e => (print "[bogus Holmakefile in current directory \
175  
-                                 \- ignoring it]\n";
176  
-                           TextIO.flushOut TextIO.stdErr;
177  
-                           ())
178  
-        else ();
  162
+use (OS.Path.concat (HOLDIR, OS.Path.concat("tools", "makefile-includes.ML")));
179 163
 
180 164
 val _ =
181 165
   (term_pp_prefix := "``";   term_pp_suffix := "``";
@@ -205,4 +189,3 @@ use (Path.concat(Globals.HOLDIR, "tools/check-intconfig.sml"));
205 189
 val _ = set_trace "pp_annotations" 1
206 190
 
207 191
 val _ = PolyML.print_depth 100;
208  
-
24  tools/makefile-includes.ML
... ...
@@ -0,0 +1,24 @@
  1
+fun extend envlist s f = let
  2
+  open Holmake_types
  3
+in
  4
+  case envlist s of
  5
+    [] => ()
  6
+  | v => (print ("[extending loadPath with Holmakefile "^s^" variable]\n");
  7
+          loadPath := f (!loadPath, v))
  8
+end
  9
+
  10
+
  11
+val _ = if FileSys.access ("Holmakefile", [FileSys.A_READ]) then let
  12
+            open Holmake_types
  13
+            val (env, _, _) = ReadHMF.read "Holmakefile" base_environment
  14
+            fun envlist id =
  15
+                map dequote (tokenize (perform_substitution env [VREF id]))
  16
+          in
  17
+            extend envlist "INCLUDES" (op@);
  18
+            extend envlist "PRE_INCLUDES" (fn (lp, mfv) => mfv @ lp)
  19
+          end
  20
+          handle e => (print "[bogus Holmakefile in current directory \
  21
+                             \- ignoring it]\n";
  22
+                       TextIO.flushOut TextIO.stdErr;
  23
+                       ())
  24
+        else ();

0 notes on commit ac14643

Please sign in to comment.
Something went wrong with that request. Please try again.