moved Thy/session.ML to Isar/session.ML;
authorwenzelm
Thu Mar 11 12:32:40 1999 +0100 (1999-03-11)
changeset 6346643a1bd31a91
parent 6345 f4a3c3bb3e38
child 6347 ce7ab97a8e15
moved Thy/session.ML to Isar/session.ML;
src/Pure/IsaMakefile
src/Pure/Isar/ROOT.ML
src/Pure/Isar/session.ML
src/Pure/Thy/ROOT.ML
src/Pure/Thy/session.ML
     1.1 --- a/src/Pure/IsaMakefile	Wed Mar 10 17:24:26 1999 +0100
     1.2 +++ b/src/Pure/IsaMakefile	Thu Mar 11 12:32:40 1999 +0100
     1.3 @@ -32,19 +32,19 @@
     1.4    Isar/isar_thy.ML Isar/method.ML Isar/outer_lex.ML \
     1.5    Isar/outer_parse.ML Isar/outer_syntax.ML Isar/proof.ML \
     1.6    Isar/proof_context.ML Isar/proof_data.ML Isar/proof_history.ML \
     1.7 -  Isar/toplevel.ML ML-Systems/mlworks.ML ML-Systems/polyml.ML \
     1.8 -  ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML ROOT.ML Syntax/ROOT.ML \
     1.9 -  Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \
    1.10 -  Syntax/printer.ML Syntax/syn_ext.ML Syntax/syn_trans.ML \
    1.11 -  Syntax/syntax.ML Syntax/token_trans.ML Syntax/type_ext.ML \
    1.12 -  Thy/ROOT.ML Thy/browser_info.ML Thy/html.ML Thy/present.ML \
    1.13 -  Thy/session.ML Thy/thm_database.ML Thy/thy_info.ML Thy/thy_load.ML \
    1.14 -  Thy/thy_parse.ML Thy/thy_scan.ML Thy/thy_syn.ML axclass.ML basis.ML \
    1.15 -  context.ML deriv.ML display.ML drule.ML envir.ML goals.ML \
    1.16 -  install_pp.ML library.ML locale.ML logic.ML net.ML object_logic.ML \
    1.17 -  pattern.ML pure.ML pure_thy.ML search.ML sign.ML sorts.ML tactic.ML \
    1.18 -  tctical.ML term.ML theory.ML theory_data.ML thm.ML type.ML \
    1.19 -  type_infer.ML unify.ML
    1.20 +  Isar/session.ML Isar/toplevel.ML ML-Systems/mlworks.ML \
    1.21 +  ML-Systems/polyml.ML ML-Systems/smlnj-0.93.ML ML-Systems/smlnj.ML \
    1.22 +  ROOT.ML Syntax/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML \
    1.23 +  Syntax/mixfix.ML Syntax/parser.ML Syntax/printer.ML \
    1.24 +  Syntax/syn_ext.ML Syntax/syn_trans.ML Syntax/syntax.ML \
    1.25 +  Syntax/token_trans.ML Syntax/type_ext.ML Thy/ROOT.ML \
    1.26 +  Thy/browser_info.ML Thy/html.ML Thy/present.ML Thy/thm_database.ML \
    1.27 +  Thy/thy_info.ML Thy/thy_load.ML Thy/thy_parse.ML Thy/thy_scan.ML \
    1.28 +  Thy/thy_syn.ML axclass.ML basis.ML context.ML deriv.ML display.ML \
    1.29 +  drule.ML envir.ML goals.ML install_pp.ML library.ML locale.ML \
    1.30 +  logic.ML net.ML object_logic.ML pattern.ML pure.ML pure_thy.ML \
    1.31 +  search.ML sign.ML sorts.ML tactic.ML tctical.ML term.ML theory.ML \
    1.32 +  theory_data.ML thm.ML type.ML type_infer.ML unify.ML
    1.33  	@./mk
    1.34  
    1.35  
     2.1 --- a/src/Pure/Isar/ROOT.ML	Wed Mar 10 17:24:26 1999 +0100
     2.2 +++ b/src/Pure/Isar/ROOT.ML	Thu Mar 11 12:32:40 1999 +0100
     2.3 @@ -9,6 +9,7 @@
     2.4  use "proof_context.ML";
     2.5  use "proof.ML";
     2.6  use "proof_data.ML";
     2.7 +use "proof_history.ML";
     2.8  use "args.ML";
     2.9  use "attrib.ML";
    2.10  use "method.ML";
    2.11 @@ -17,9 +18,9 @@
    2.12  use "outer_lex.ML";
    2.13  use "outer_parse.ML";
    2.14  
    2.15 -(*interactive subsystem*)
    2.16 -use "proof_history.ML";
    2.17 +(*toplevel environment*)
    2.18  use "toplevel.ML";
    2.19 +use "session.ML";
    2.20  
    2.21  (*theory operations*)
    2.22  use "isar_thy.ML";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Isar/session.ML	Thu Mar 11 12:32:40 1999 +0100
     3.3 @@ -0,0 +1,68 @@
     3.4 +(*  Title:      Pure/Isar/session.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Markus Wenzel, TU Muenchen
     3.7 +
     3.8 +Session management -- maintain state of logic images.
     3.9 +*)
    3.10 +
    3.11 +signature SESSION =
    3.12 +sig
    3.13 +  val welcome: unit -> string
    3.14 +  val use_dir: bool -> bool -> string -> string -> unit
    3.15 +  val finish: unit -> unit
    3.16 +end;
    3.17 +
    3.18 +structure Session: SESSION =
    3.19 +struct
    3.20 +
    3.21 +
    3.22 +(* session state *)
    3.23 +
    3.24 +val pure = "Pure";
    3.25 +
    3.26 +val session = ref ([pure]: string list);
    3.27 +val session_path = ref ([]: string list);
    3.28 +val session_finished = ref false;
    3.29 +
    3.30 +fun path () = ! session_path;
    3.31 +
    3.32 +fun add_path reset s =
    3.33 +  (session := ! session @ [s]; session_path := ((if reset then [] else ! session_path) @ [s]));
    3.34 +
    3.35 +
    3.36 +(* diagnostics *)
    3.37 +
    3.38 +fun str_of [] = "Pure"
    3.39 +  | str_of elems = space_implode "/" elems;
    3.40 +
    3.41 +fun welcome () = "Welcome to Isabelle/" ^ str_of (path ()) ^ " (" ^ version ^ ")";
    3.42 +
    3.43 +
    3.44 +(* init *)
    3.45 +
    3.46 +fun init reset parent name =
    3.47 +  if not (parent mem_string (! session)) orelse not (! session_finished) then
    3.48 +    error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
    3.49 +  else (add_path reset name; session_finished := false);
    3.50 +
    3.51 +
    3.52 +(* finish *)
    3.53 +
    3.54 +fun finish () =
    3.55 +  (ThyInfo.finalize_all ();
    3.56 +    Present.finish ();
    3.57 +    session_finished := true);
    3.58 +
    3.59 +
    3.60 +(* use_dir *)
    3.61 +
    3.62 +val root_file = ThyLoad.ml_path "ROOT";
    3.63 +
    3.64 +fun use_dir reset info parent name =
    3.65 +  (init reset parent name;
    3.66 +    Present.init info (path ()) name;
    3.67 +    Symbol.use root_file;
    3.68 +    finish ()) handle exn => (writeln (Toplevel.exn_message exn); exit 1);
    3.69 +
    3.70 +
    3.71 +end;
     4.1 --- a/src/Pure/Thy/ROOT.ML	Wed Mar 10 17:24:26 1999 +0100
     4.2 +++ b/src/Pure/Thy/ROOT.ML	Thu Mar 11 12:32:40 1999 +0100
     4.3 @@ -14,8 +14,6 @@
     4.4  use "present.ML";
     4.5  use "thm_database.ML";
     4.6  
     4.7 -use "session.ML";
     4.8 -
     4.9  (*theory syntax (old format)*)
    4.10  use "thy_scan.ML";
    4.11  use "thy_parse.ML";
     5.1 --- a/src/Pure/Thy/session.ML	Wed Mar 10 17:24:26 1999 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,68 +0,0 @@
     5.4 -(*  Title:      Pure/Thy/session.ML
     5.5 -    ID:         $Id$
     5.6 -    Author:     Markus Wenzel, TU Muenchen
     5.7 -
     5.8 -Session management -- maintain state of logic images.
     5.9 -*)
    5.10 -
    5.11 -signature SESSION =
    5.12 -sig
    5.13 -  val welcome: unit -> string
    5.14 -  val use_dir: bool -> bool -> string -> string -> unit
    5.15 -  val finish: unit -> unit
    5.16 -end;
    5.17 -
    5.18 -structure Session: SESSION =
    5.19 -struct
    5.20 -
    5.21 -
    5.22 -(* session state *)
    5.23 -
    5.24 -val pure = "Pure";
    5.25 -
    5.26 -val session = ref ([pure]: string list);
    5.27 -val session_path = ref ([]: string list);
    5.28 -val session_finished = ref false;
    5.29 -
    5.30 -fun path () = ! session_path;
    5.31 -
    5.32 -fun add_path reset s =
    5.33 -  (session := ! session @ [s]; session_path := ((if reset then [] else ! session_path) @ [s]));
    5.34 -
    5.35 -
    5.36 -(* diagnostics *)
    5.37 -
    5.38 -fun str_of [] = "Pure"
    5.39 -  | str_of elems = space_implode "/" elems;
    5.40 -
    5.41 -fun welcome () = "Welcome to Isabelle/" ^ str_of (path ()) ^ " (" ^ version ^ ")";
    5.42 -
    5.43 -
    5.44 -(* init *)
    5.45 -
    5.46 -fun init reset parent name =
    5.47 -  if not (parent mem_string (! session)) orelse not (! session_finished) then
    5.48 -    error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
    5.49 -  else (add_path reset name; session_finished := false);
    5.50 -
    5.51 -
    5.52 -(* finish *)
    5.53 -
    5.54 -fun finish () =
    5.55 -  (ThyInfo.finalize_all ();
    5.56 -    Present.finish ();
    5.57 -    session_finished := true);
    5.58 -
    5.59 -
    5.60 -(* use_dir *)
    5.61 -
    5.62 -val root_file = ThyLoad.ml_path "ROOT";
    5.63 -
    5.64 -fun use_dir reset info parent name =
    5.65 -  (init reset parent name;
    5.66 -    Present.init info (path ()) name;
    5.67 -    Symbol.use root_file;
    5.68 -    finish ()) handle _ => exit 1;
    5.69 -
    5.70 -
    5.71 -end;