# HG changeset patch # User wenzelm # Date 921151960 -3600 # Node ID 643a1bd31a913c48cd526d9828a4440f9229eeb9 # Parent f4a3c3bb3e38b93728ee876b8eec2fe4b6d8c7b7 moved Thy/session.ML to Isar/session.ML; diff -r f4a3c3bb3e38 -r 643a1bd31a91 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Wed Mar 10 17:24:26 1999 +0100 +++ b/src/Pure/IsaMakefile Thu Mar 11 12:32:40 1999 +0100 @@ -32,19 +32,19 @@ Isar/isar_thy.ML Isar/method.ML Isar/outer_lex.ML \ Isar/outer_parse.ML Isar/outer_syntax.ML Isar/proof.ML \ Isar/proof_context.ML Isar/proof_data.ML Isar/proof_history.ML \ - Isar/toplevel.ML ML-Systems/mlworks.ML ML-Systems/polyml.ML \ - ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML ROOT.ML Syntax/ROOT.ML \ - Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \ - Syntax/printer.ML Syntax/syn_ext.ML Syntax/syn_trans.ML \ - Syntax/syntax.ML Syntax/token_trans.ML Syntax/type_ext.ML \ - Thy/ROOT.ML Thy/browser_info.ML Thy/html.ML Thy/present.ML \ - Thy/session.ML Thy/thm_database.ML Thy/thy_info.ML Thy/thy_load.ML \ - Thy/thy_parse.ML Thy/thy_scan.ML Thy/thy_syn.ML axclass.ML basis.ML \ - context.ML deriv.ML display.ML drule.ML envir.ML goals.ML \ - install_pp.ML library.ML locale.ML logic.ML net.ML object_logic.ML \ - pattern.ML pure.ML pure_thy.ML search.ML sign.ML sorts.ML tactic.ML \ - tctical.ML term.ML theory.ML theory_data.ML thm.ML type.ML \ - type_infer.ML unify.ML + Isar/session.ML Isar/toplevel.ML ML-Systems/mlworks.ML \ + ML-Systems/polyml.ML ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML \ + ROOT.ML Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML \ + Syntax/mixfix.ML Syntax/parser.ML Syntax/printer.ML \ + Syntax/syn_ext.ML Syntax/syn_trans.ML Syntax/syntax.ML \ + Syntax/token_trans.ML Syntax/type_ext.ML Thy/ROOT.ML \ + Thy/browser_info.ML Thy/html.ML Thy/present.ML Thy/thm_database.ML \ + Thy/thy_info.ML Thy/thy_load.ML Thy/thy_parse.ML Thy/thy_scan.ML \ + Thy/thy_syn.ML axclass.ML basis.ML context.ML deriv.ML display.ML \ + drule.ML envir.ML goals.ML install_pp.ML library.ML locale.ML \ + logic.ML net.ML object_logic.ML pattern.ML pure.ML pure_thy.ML \ + search.ML sign.ML sorts.ML tactic.ML tctical.ML term.ML theory.ML \ + theory_data.ML thm.ML type.ML type_infer.ML unify.ML @./mk diff -r f4a3c3bb3e38 -r 643a1bd31a91 src/Pure/Isar/ROOT.ML --- a/src/Pure/Isar/ROOT.ML Wed Mar 10 17:24:26 1999 +0100 +++ b/src/Pure/Isar/ROOT.ML Thu Mar 11 12:32:40 1999 +0100 @@ -9,6 +9,7 @@ use "proof_context.ML"; use "proof.ML"; use "proof_data.ML"; +use "proof_history.ML"; use "args.ML"; use "attrib.ML"; use "method.ML"; @@ -17,9 +18,9 @@ use "outer_lex.ML"; use "outer_parse.ML"; -(*interactive subsystem*) -use "proof_history.ML"; +(*toplevel environment*) use "toplevel.ML"; +use "session.ML"; (*theory operations*) use "isar_thy.ML"; diff -r f4a3c3bb3e38 -r 643a1bd31a91 src/Pure/Isar/session.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Isar/session.ML Thu Mar 11 12:32:40 1999 +0100 @@ -0,0 +1,68 @@ +(* Title: Pure/Isar/session.ML + ID: $Id$ + Author: Markus Wenzel, TU Muenchen + +Session management -- maintain state of logic images. +*) + +signature SESSION = +sig + val welcome: unit -> string + val use_dir: bool -> bool -> string -> string -> unit + val finish: unit -> unit +end; + +structure Session: SESSION = +struct + + +(* session state *) + +val pure = "Pure"; + +val session = ref ([pure]: string list); +val session_path = ref ([]: string list); +val session_finished = ref false; + +fun path () = ! session_path; + +fun add_path reset s = + (session := ! session @ [s]; session_path := ((if reset then [] else ! session_path) @ [s])); + + +(* diagnostics *) + +fun str_of [] = "Pure" + | str_of elems = space_implode "/" elems; + +fun welcome () = "Welcome to Isabelle/" ^ str_of (path ()) ^ " (" ^ version ^ ")"; + + +(* init *) + +fun init reset parent name = + if not (parent mem_string (! session)) orelse not (! session_finished) then + error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name) + else (add_path reset name; session_finished := false); + + +(* finish *) + +fun finish () = + (ThyInfo.finalize_all (); + Present.finish (); + session_finished := true); + + +(* use_dir *) + +val root_file = ThyLoad.ml_path "ROOT"; + +fun use_dir reset info parent name = + (init reset parent name; + Present.init info (path ()) name; + Symbol.use root_file; + finish ()) handle exn => (writeln (Toplevel.exn_message exn); exit 1); + + +end; diff -r f4a3c3bb3e38 -r 643a1bd31a91 src/Pure/Thy/ROOT.ML --- a/src/Pure/Thy/ROOT.ML Wed Mar 10 17:24:26 1999 +0100 +++ b/src/Pure/Thy/ROOT.ML Thu Mar 11 12:32:40 1999 +0100 @@ -14,8 +14,6 @@ use "present.ML"; use "thm_database.ML"; -use "session.ML"; - (*theory syntax (old format)*) use "thy_scan.ML"; use "thy_parse.ML"; diff -r f4a3c3bb3e38 -r 643a1bd31a91 src/Pure/Thy/session.ML --- a/src/Pure/Thy/session.ML Wed Mar 10 17:24:26 1999 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,68 +0,0 @@ -(* Title: Pure/Thy/session.ML - ID: $Id$ - Author: Markus Wenzel, TU Muenchen - -Session management -- maintain state of logic images. -*) - -signature SESSION = -sig - val welcome: unit -> string - val use_dir: bool -> bool -> string -> string -> unit - val finish: unit -> unit -end; - -structure Session: SESSION = -struct - - -(* session state *) - -val pure = "Pure"; - -val session = ref ([pure]: string list); -val session_path = ref ([]: string list); -val session_finished = ref false; - -fun path () = ! session_path; - -fun add_path reset s = - (session := ! session @ [s]; session_path := ((if reset then [] else ! session_path) @ [s])); - - -(* diagnostics *) - -fun str_of [] = "Pure" - | str_of elems = space_implode "/" elems; - -fun welcome () = "Welcome to Isabelle/" ^ str_of (path ()) ^ " (" ^ version ^ ")"; - - -(* init *) - -fun init reset parent name = - if not (parent mem_string (! session)) orelse not (! session_finished) then - error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name) - else (add_path reset name; session_finished := false); - - -(* finish *) - -fun finish () = - (ThyInfo.finalize_all (); - Present.finish (); - session_finished := true); - - -(* use_dir *) - -val root_file = ThyLoad.ml_path "ROOT"; - -fun use_dir reset info parent name = - (init reset parent name; - Present.init info (path ()) name; - Symbol.use root_file; - finish ()) handle _ => exit 1; - - -end;