1.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Oct 26 22:34:01 1999 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Oct 26 22:36:50 1999 +0200
     1.3 @@ -55,7 +55,7 @@
     1.4    val add_keywords: string list -> unit
     1.5    val add_parsers: parser list -> unit
     1.6    val theory_header: token list -> (string * string list * (string * bool) list) * token list
     1.7 -  val deps_thy: string -> Path.T -> string list * Path.T list
     1.8 +  val deps_thy: string -> bool -> Path.T -> string list * Path.T list
     1.9    val load_thy: string -> bool -> bool -> Path.T -> unit
    1.10    val isar: bool -> bool -> Toplevel.isar
    1.11  end;
    1.12 @@ -314,21 +314,22 @@
    1.13      (P.name -- (P.$$$ "=" |-- P.name -- Scan.repeat (P.$$$ "+" |-- P.name))))
    1.14    >> (fn (A, (B, Bs)) => (A, B :: Bs, []: (string * bool) list));
    1.15  
    1.16 -fun deps_thy name path =
    1.17 +fun deps_thy name ml path =
    1.18    let
    1.19      val src = Source.of_string (File.read path);
    1.20      val pos = Path.position path;
    1.21      val (name', parents, files) =
    1.22 -      (*Note: old style headers dynamically depend on the current lexicon :-( *)
    1.23 +      (*unfortunately, old-style headers dynamically depend on the current lexicon*)
    1.24        if is_old_theory (src, pos) then
    1.25          scan_header ThySyn.get_lexicon (Scan.error old_header) (src, pos)
    1.26        else scan_header (K header_lexicon) (Scan.error new_header) (src, pos);
    1.27  
    1.28      val ml_path = ThyLoad.ml_path name;
    1.29 -    val ml_file = if is_none (ThyLoad.check_file ml_path) then [] else [ml_path];
    1.30 +    val ml_file = if ml andalso is_some (ThyLoad.check_file ml_path) then [ml_path] else [];
    1.31    in
    1.32      if name <> name' then
    1.33 -      error ("Filename " ^ quote (Path.pack path) ^ " does not match theory name " ^ quote name)
    1.34 +      error ("Filename " ^ quote (Path.pack path) ^
    1.35 +        " does not agree with theory name " ^ quote name)
    1.36      else (parents, map (Path.unpack o #1) files @ ml_file)
    1.37    end;
    1.38  
    1.39 @@ -377,10 +378,10 @@
    1.40  
    1.41  local
    1.42  
    1.43 -fun try_ml_file name ml time =
    1.44 +fun try_ml_file name time =
    1.45    let
    1.46      val path = ThyLoad.ml_path name;
    1.47 -    val tr = Toplevel.imperative (fn () => ThyInfo.may_load_file ml time path);
    1.48 +    val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path);
    1.49      val tr_name = if time then "time_use" else "use";
    1.50    in
    1.51      if is_none (ThyLoad.check_file path) then ()
    1.52 @@ -417,7 +418,7 @@
    1.53        writeln ("**** Finished theory " ^ quote name ^ " ****\n")))
    1.54    else run_thy name path;
    1.55    Context.context (ThyInfo.get_theory name);
    1.56 -  try_ml_file name ml time);
    1.57 +  if ml then try_ml_file name time else ());
    1.58  
    1.59  end;
    1.60  
    1.61 @@ -444,7 +445,6 @@
    1.62  
    1.63  fun gen_main term no_pos =
    1.64   (Toplevel.set_state Toplevel.toplevel;
    1.65 -  ml_prompts "ML> " "ML# ";
    1.66    writeln (Session.welcome ());
    1.67    gen_loop term no_pos);
    1.68