# HG changeset patch # User wenzelm # Date 940970210 -7200 # Node ID def6db2399348658f099f407be5620ce8127bba1 # Parent 131a2c54036fa56b3abbb0b6b3c168fd4dccc804 improved ml handling; diff -r 131a2c54036f -r def6db239934 src/Pure/Isar/outer_syntax.ML --- 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); diff -r 131a2c54036f -r def6db239934 src/Pure/Thy/thy_load.ML --- 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;