improved ml handling;

--- a/src/Pure/Isar/outer_syntax.ML	Tue Oct 26 22:34:01 1999 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Oct 26 22:36:50 1999 +0200
@@ -55,7 +55,7 @@
   val add_keywords: string list -> unit
   val add_parsers: parser list -> unit
   val theory_header: token list -> (string * string list * (string * bool) list) * token list
-  val deps_thy: string -> Path.T -> string list * Path.T list
+  val deps_thy: string -> bool -> Path.T -> string list * Path.T list
   val load_thy: string -> bool -> bool -> Path.T -> unit
   val isar: bool -> bool -> Toplevel.isar
 end;
@@ -314,21 +314,22 @@
     (P.name -- (P.$$$ "=" |-- P.name -- Scan.repeat (P.$$$ "+" |-- P.name))))
   >> (fn (A, (B, Bs)) => (A, B :: Bs, []: (string * bool) list));
 
-fun deps_thy name path =
+fun deps_thy name ml path =
   let
     val src = Source.of_string (File.read path);
     val pos = Path.position path;
     val (name', parents, files) =
-      (*Note: old style headers dynamically depend on the current lexicon :-( *)
+      (*unfortunately, old-style headers dynamically depend on the current lexicon*)
       if is_old_theory (src, pos) then
         scan_header ThySyn.get_lexicon (Scan.error old_header) (src, pos)
       else scan_header (K header_lexicon) (Scan.error new_header) (src, pos);
 
     val ml_path = ThyLoad.ml_path name;
-    val ml_file = if is_none (ThyLoad.check_file ml_path) then [] else [ml_path];
+    val ml_file = if ml andalso is_some (ThyLoad.check_file ml_path) then [ml_path] else [];
   in
     if name <> name' then
-      error ("Filename " ^ quote (Path.pack path) ^ " does not match theory name " ^ quote name)
+      error ("Filename " ^ quote (Path.pack path) ^
+        " does not agree with theory name " ^ quote name)
     else (parents, map (Path.unpack o #1) files @ ml_file)
   end;
 
@@ -377,10 +378,10 @@
 
 local
 
-fun try_ml_file name ml time =
+fun try_ml_file name time =
   let
     val path = ThyLoad.ml_path name;
-    val tr = Toplevel.imperative (fn () => ThyInfo.may_load_file ml time path);
+    val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path);
     val tr_name = if time then "time_use" else "use";
   in
     if is_none (ThyLoad.check_file path) then ()
@@ -417,7 +418,7 @@
       writeln ("**** Finished theory " ^ quote name ^ " ****\n")))
   else run_thy name path;
   Context.context (ThyInfo.get_theory name);
-  try_ml_file name ml time);
+  if ml then try_ml_file name time else ());
 
 end;
 
@@ -444,7 +445,6 @@
 
 fun gen_main term no_pos =
  (Toplevel.set_state Toplevel.toplevel;
-  ml_prompts "ML> " "ML# ";
   writeln (Session.welcome ());
   gen_loop term no_pos);
 

--- a/src/Pure/Thy/thy_load.ML	Tue Oct 26 22:34:01 1999 +0200
+++ b/src/Pure/Thy/thy_load.ML	Tue Oct 26 22:36:50 1999 +0200
@@ -20,19 +20,19 @@
   val ml_path: string -> Path.T
   val thy_path: string -> Path.T
   val check_file: Path.T -> (Path.T * File.info) option
-  val may_load_file: bool -> Path.T -> (Path.T * File.info)
+  val load_file: Path.T -> (Path.T * File.info)
   eqtype master
   val get_thy: master -> Path.T * File.info
-  val check_thy: Path.T -> string -> master
-  val deps_thy: Path.T -> string -> master * (string list * Path.T list)
+  val check_thy: Path.T -> string -> bool -> master
+  val deps_thy: Path.T -> string -> bool -> master * (string list * Path.T list)
   val load_thy: Path.T -> string -> bool -> bool -> master
 end;
 
-(*backdoor sealed later*)
+(*this backdoor sealed later*)
 signature PRIVATE_THY_LOAD =
 sig
   include THY_LOAD
-  val deps_thy_fn: (string -> Path.T -> string list * Path.T list) ref
+  val deps_thy_fn: (string -> bool -> Path.T -> string list * Path.T list) ref
   val load_thy_fn: (string -> bool -> bool -> Path.T -> unit) ref
 end;
 
@@ -77,12 +77,12 @@
   in get_first find_dir (if Path.is_basic path then ! load_path else [Path.current]) end;
 
 
-(* may_load_file *)
+(* load_file *)
 
-fun may_load_file really raw_path =
+fun load_file raw_path =
   (case check_file raw_path of
     None => error ("Could not find ML file " ^ quote (Path.pack raw_path))
-  | Some (path, info) => (if really then File.symbol_use path else (); (path, info)));
+  | Some (path, info) => (File.symbol_use path; (path, info)));
 
 
 (* datatype master *)
@@ -92,30 +92,36 @@
 fun get_thy (Master (thy, _)) = thy;
 
 
-(* check_thy *)
+(* check / process theory files *)
 
-fun check_thy_aux name =
+local
+
+fun check_thy_aux (name, ml) =
   (case check_file (thy_path name) of
     None => error ("Could not find theory file for " ^ quote name ^ " in dir(s) " ^
       commas_quote (show_path ()))
-  | Some thy_info => (thy_info, check_file (ml_path name)));
+  | Some thy_info => (thy_info, if ml then check_file (ml_path name) else None));
+
+in
+
+fun check_thy dir name ml = Master (cond_with_path dir check_thy_aux (name, ml));
 
-fun check_thy dir name = Master (cond_with_path dir check_thy_aux name);
+fun process_thy dir f name ml =
+  let val master as Master ((path, _), _) = check_thy dir name ml
+  in (master, cond_with_path dir f path) end;
+
+end;
 
 
-(* process theory files *)
+(* deps_thy and load_thy *)
 
 (*hooks for theory syntax dependent operations*)
 fun undefined _ = raise Match;
-val deps_thy_fn = ref (undefined: string -> Path.T -> string list * Path.T list);
+val deps_thy_fn = ref (undefined: string -> bool -> Path.T -> string list * Path.T list);
 val load_thy_fn = ref (undefined: string -> bool -> bool -> Path.T -> unit);
 
-fun process_thy dir f name =
-  let val master as Master ((path, _), _) = check_thy dir name
-  in (master, cond_with_path dir f path) end;
-
-fun deps_thy dir name = process_thy dir (! deps_thy_fn name) name;
-fun load_thy dir name ml time = #1 (process_thy dir (! load_thy_fn name ml time) name);
+fun deps_thy dir name ml = process_thy dir (! deps_thy_fn name ml) name ml;
+fun load_thy dir name ml time = #1 (process_thy dir (! load_thy_fn name ml time) name ml);
 
 
 end;