improved ml handling;
authorwenzelm
Tue Oct 26 22:36:50 1999 +0200 (1999-10-26 ago)
changeset 7940def6db239934
parent 7939 131a2c54036f
child 7941 653964583bd3
improved ml handling;
src/Pure/Isar/outer_syntax.ML
src/Pure/Thy/thy_load.ML
     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  
     2.1 --- a/src/Pure/Thy/thy_load.ML	Tue Oct 26 22:34:01 1999 +0200
     2.2 +++ b/src/Pure/Thy/thy_load.ML	Tue Oct 26 22:36:50 1999 +0200
     2.3 @@ -20,19 +20,19 @@
     2.4    val ml_path: string -> Path.T
     2.5    val thy_path: string -> Path.T
     2.6    val check_file: Path.T -> (Path.T * File.info) option
     2.7 -  val may_load_file: bool -> Path.T -> (Path.T * File.info)
     2.8 +  val load_file: Path.T -> (Path.T * File.info)
     2.9    eqtype master
    2.10    val get_thy: master -> Path.T * File.info
    2.11 -  val check_thy: Path.T -> string -> master
    2.12 -  val deps_thy: Path.T -> string -> master * (string list * Path.T list)
    2.13 +  val check_thy: Path.T -> string -> bool -> master
    2.14 +  val deps_thy: Path.T -> string -> bool -> master * (string list * Path.T list)
    2.15    val load_thy: Path.T -> string -> bool -> bool -> master
    2.16  end;
    2.17  
    2.18 -(*backdoor sealed later*)
    2.19 +(*this backdoor sealed later*)
    2.20  signature PRIVATE_THY_LOAD =
    2.21  sig
    2.22    include THY_LOAD
    2.23 -  val deps_thy_fn: (string -> Path.T -> string list * Path.T list) ref
    2.24 +  val deps_thy_fn: (string -> bool -> Path.T -> string list * Path.T list) ref
    2.25    val load_thy_fn: (string -> bool -> bool -> Path.T -> unit) ref
    2.26  end;
    2.27  
    2.28 @@ -77,12 +77,12 @@
    2.29    in get_first find_dir (if Path.is_basic path then ! load_path else [Path.current]) end;
    2.30  
    2.31  
    2.32 -(* may_load_file *)
    2.33 +(* load_file *)
    2.34  
    2.35 -fun may_load_file really raw_path =
    2.36 +fun load_file raw_path =
    2.37    (case check_file raw_path of
    2.38      None => error ("Could not find ML file " ^ quote (Path.pack raw_path))
    2.39 -  | Some (path, info) => (if really then File.symbol_use path else (); (path, info)));
    2.40 +  | Some (path, info) => (File.symbol_use path; (path, info)));
    2.41  
    2.42  
    2.43  (* datatype master *)
    2.44 @@ -92,30 +92,36 @@
    2.45  fun get_thy (Master (thy, _)) = thy;
    2.46  
    2.47  
    2.48 -(* check_thy *)
    2.49 +(* check / process theory files *)
    2.50  
    2.51 -fun check_thy_aux name =
    2.52 +local
    2.53 +
    2.54 +fun check_thy_aux (name, ml) =
    2.55    (case check_file (thy_path name) of
    2.56      None => error ("Could not find theory file for " ^ quote name ^ " in dir(s) " ^
    2.57        commas_quote (show_path ()))
    2.58 -  | Some thy_info => (thy_info, check_file (ml_path name)));
    2.59 +  | Some thy_info => (thy_info, if ml then check_file (ml_path name) else None));
    2.60 +
    2.61 +in
    2.62 +
    2.63 +fun check_thy dir name ml = Master (cond_with_path dir check_thy_aux (name, ml));
    2.64  
    2.65 -fun check_thy dir name = Master (cond_with_path dir check_thy_aux name);
    2.66 +fun process_thy dir f name ml =
    2.67 +  let val master as Master ((path, _), _) = check_thy dir name ml
    2.68 +  in (master, cond_with_path dir f path) end;
    2.69 +
    2.70 +end;
    2.71  
    2.72  
    2.73 -(* process theory files *)
    2.74 +(* deps_thy and load_thy *)
    2.75  
    2.76  (*hooks for theory syntax dependent operations*)
    2.77  fun undefined _ = raise Match;
    2.78 -val deps_thy_fn = ref (undefined: string -> Path.T -> string list * Path.T list);
    2.79 +val deps_thy_fn = ref (undefined: string -> bool -> Path.T -> string list * Path.T list);
    2.80  val load_thy_fn = ref (undefined: string -> bool -> bool -> Path.T -> unit);
    2.81  
    2.82 -fun process_thy dir f name =
    2.83 -  let val master as Master ((path, _), _) = check_thy dir name
    2.84 -  in (master, cond_with_path dir f path) end;
    2.85 -
    2.86 -fun deps_thy dir name = process_thy dir (! deps_thy_fn name) name;
    2.87 -fun load_thy dir name ml time = #1 (process_thy dir (! load_thy_fn name ml time) name);
    2.88 +fun deps_thy dir name ml = process_thy dir (! deps_thy_fn name ml) name ml;
    2.89 +fun load_thy dir name ml time = #1 (process_thy dir (! load_thy_fn name ml time) name ml);
    2.90  
    2.91  
    2.92  end;