Skip to content
Browse files

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...
1 parent aa4e6aa commit ac146436031e6baf322b37f999cae02e55cce7e3 @mn200 mn200 committed
Showing with 26 additions and 35 deletions.
  1. +1 −17 std.prelude
  2. +1 −18 tools-poly/prelude.ML
  3. +24 −0 tools/makefile-includes.ML
View
18 std.prelude
@@ -167,23 +167,7 @@ in
val _ = loadPath := tl (!loadPath)
end;
-val _ = if FileSys.access ("Holmakefile", [FileSys.A_READ]) then let
- open Holmake_types
- val (env, _, _) = ReadHMF.read "Holmakefile" base_environment
- fun envlist id =
- map dequote (tokenize (perform_substitution env [VREF id]))
- val hmake_includes = envlist "INCLUDES"
- in
- case hmake_includes of
- [] => ()
- | _ =>
- (print "[extending loadPath with Holmakefile INCLUDES variable]\n";
- loadPath := !loadPath @ hmake_includes)
- end handle e => (print "[bogus Holmakefile in current directory \
- \- ignoring it]\n";
- TextIO.flushOut TextIO.stdErr;
- ())
- else ()
+use (OS.Path.concat (HOLDIR, OS.Path.concat("tools", "makefile-includes.ML")));
structure HOL_Interactive : sig
val toggle_quietdec : unit -> bool
View
19 tools-poly/prelude.ML
@@ -159,23 +159,7 @@ in
app appthis ["internal_functions", "Holmake_types", "ReadHMF"]
end;
-val _ = if FileSys.access ("Holmakefile", [FileSys.A_READ]) then let
- open Holmake_types
- val (env, _, _) = ReadHMF.read "Holmakefile" base_environment
- fun envlist id =
- map dequote (tokenize (perform_substitution env [VREF id]))
- val hmake_includes = envlist "INCLUDES"
- in
- case hmake_includes of
- [] => ()
- | _ =>
- (print "[extending loadPath with Holmakefile INCLUDES variable]\n";
- loadPath := !loadPath @ hmake_includes)
- end handle e => (print "[bogus Holmakefile in current directory \
- \- ignoring it]\n";
- TextIO.flushOut TextIO.stdErr;
- ())
- else ();
+use (OS.Path.concat (HOLDIR, OS.Path.concat("tools", "makefile-includes.ML")));
val _ =
(term_pp_prefix := "``"; term_pp_suffix := "``";
@@ -205,4 +189,3 @@ use (Path.concat(Globals.HOLDIR, "tools/check-intconfig.sml"));
val _ = set_trace "pp_annotations" 1
val _ = PolyML.print_depth 100;
-
View
24 tools/makefile-includes.ML
@@ -0,0 +1,24 @@
+fun extend envlist s f = let
+ open Holmake_types
+in
+ case envlist s of
+ [] => ()
+ | v => (print ("[extending loadPath with Holmakefile "^s^" variable]\n");
+ loadPath := f (!loadPath, v))
+end
+
+
+val _ = if FileSys.access ("Holmakefile", [FileSys.A_READ]) then let
+ open Holmake_types
+ val (env, _, _) = ReadHMF.read "Holmakefile" base_environment
+ fun envlist id =
+ map dequote (tokenize (perform_substitution env [VREF id]))
+ in
+ extend envlist "INCLUDES" (op@);
+ extend envlist "PRE_INCLUDES" (fn (lp, mfv) => mfv @ lp)
+ end
+ handle e => (print "[bogus Holmakefile in current directory \
+ \- ignoring it]\n";
+ TextIO.flushOut TextIO.stdErr;
+ ())
+ else ();

0 comments on commit ac14643

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