moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
--- a/src/Pure/IsaMakefile Sat Feb 28 17:09:32 2009 +0100
+++ b/src/Pure/IsaMakefile Sat Feb 28 18:00:20 2009 +0100
@@ -59,18 +59,17 @@
Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML \
Isar/class_target.ML Isar/code.ML Isar/code_unit.ML \
Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML \
- Isar/expression.ML Isar/isar.ML Isar/isar_cmd.ML \
- Isar/isar_document.ML Isar/isar_syn.ML Isar/local_defs.ML \
- Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML \
- Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML Isar/obtain.ML \
- Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML \
- Isar/outer_syntax.ML Isar/overloading.ML Isar/proof.ML \
- Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML \
- Isar/rule_cases.ML Isar/rule_insts.ML Isar/session.ML \
- Isar/skip_proof.ML Isar/spec_parse.ML Isar/specification.ML \
- Isar/theory_target.ML Isar/toplevel.ML Isar/value_parse.ML \
- ML/ml_antiquote.ML ML/ml_context.ML ML/ml_lex.ML ML/ml_parse.ML \
- ML/ml_syntax.ML ML/ml_thms.ML Proof/extraction.ML \
+ Isar/expression.ML Isar/isar_cmd.ML Isar/isar_document.ML \
+ Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML \
+ Isar/local_theory.ML Isar/locale.ML Isar/method.ML Isar/net_rules.ML \
+ Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML \
+ Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML \
+ Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML \
+ Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML \
+ Isar/rule_insts.ML Isar/skip_proof.ML Isar/spec_parse.ML \
+ Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML \
+ Isar/value_parse.ML ML/ml_antiquote.ML ML/ml_context.ML ML/ml_lex.ML \
+ ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML Proof/extraction.ML \
Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \
Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/ROOT.ML \
ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML \
@@ -81,11 +80,12 @@
ProofGeneral/proof_general_pgip.ML Pure.thy ROOT.ML Syntax/ast.ML \
Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \
Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML \
- Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML \
- Thy/latex.ML Thy/present.ML Thy/term_style.ML Thy/thm_deps.ML \
- Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML Thy/thy_output.ML \
- Thy/thy_syntax.ML Tools/ROOT.ML Tools/find_consts.ML \
- Tools/find_theorems.ML Tools/isabelle_process.ML Tools/named_thms.ML \
+ Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML \
+ System/isabelle_process.ML System/isar.ML System/session.ML \
+ Thy/html.ML Thy/latex.ML Thy/present.ML Thy/term_style.ML \
+ Thy/thm_deps.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML \
+ Thy/thy_output.ML Thy/thy_syntax.ML Tools/ROOT.ML \
+ Tools/find_consts.ML Tools/find_theorems.ML Tools/named_thms.ML \
Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML config.ML \
conjunction.ML consts.ML context.ML context_position.ML conv.ML \
defs.ML display.ML drule.ML envir.ML facts.ML goal.ML \
@@ -119,7 +119,7 @@
General/position.scala General/swing.scala General/symbol.scala \
General/xml.scala General/yxml.scala Isar/isar.scala \
Isar/isar_document.scala Isar/outer_keyword.scala \
- Thy/thy_header.scala Tools/isabelle_process.scala \
+ System/isabelle_process.scala Thy/thy_header.scala \
Tools/isabelle_syntax.scala Tools/isabelle_system.scala
--- a/src/Pure/Isar/ROOT.ML Sat Feb 28 17:09:32 2009 +0100
+++ b/src/Pure/Isar/ROOT.ML Sat Feb 28 18:00:20 2009 +0100
@@ -82,8 +82,6 @@
use "../old_goals.ML";
use "outer_syntax.ML";
use "../Thy/thy_info.ML";
-use "session.ML";
-use "isar.ML";
use "isar_document.ML";
(*theory and proof operations*)
@@ -91,3 +89,5 @@
use "../Thy/thm_deps.ML";
use "isar_cmd.ML";
use "isar_syn.ML";
+
+
--- a/src/Pure/Isar/isar.ML Sat Feb 28 17:09:32 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,379 +0,0 @@
-(* Title: Pure/Isar/isar.ML
- Author: Makarius
-
-The global Isabelle/Isar state and main read-eval-print loop.
-*)
-
-signature ISAR =
-sig
- val init: unit -> unit
- val exn: unit -> (exn * string) option
- val state: unit -> Toplevel.state
- val context: unit -> Proof.context
- val goal: unit -> thm
- val print: unit -> unit
- val >> : Toplevel.transition -> bool
- val >>> : Toplevel.transition list -> unit
- val linear_undo: int -> unit
- val undo: int -> unit
- val kill: unit -> unit
- val kill_proof: unit -> unit
- val crashes: exn list ref
- val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
- val loop: unit -> unit
- val main: unit -> unit
-
- type id = string
- val no_id: id
- val create_command: Toplevel.transition -> id
- val insert_command: id -> id -> unit
- val remove_command: id -> unit
-end;
-
-structure Isar: ISAR =
-struct
-
-
-(** TTY model -- SINGLE-THREADED! **)
-
-(* the global state *)
-
-type history = (Toplevel.state * Toplevel.transition) list;
- (*previous state, state transition -- regular commands only*)
-
-local
- val global_history = ref ([]: history);
- val global_state = ref Toplevel.toplevel;
- val global_exn = ref (NONE: (exn * string) option);
-in
-
-fun edit_history count f = NAMED_CRITICAL "Isar" (fn () =>
- let
- fun edit 0 (st, hist) = (global_history := hist; global_state := st; global_exn := NONE)
- | edit n (st, hist) = edit (n - 1) (f st hist);
- in edit count (! global_state, ! global_history) end);
-
-fun state () = NAMED_CRITICAL "Isar" (fn () => ! global_state);
-fun set_state state = NAMED_CRITICAL "Isar" (fn () => global_state := state);
-
-fun exn () = NAMED_CRITICAL "Isar" (fn () => ! global_exn);
-fun set_exn exn = NAMED_CRITICAL "Isar" (fn () => global_exn := exn);
-
-end;
-
-
-fun init () = edit_history 1 (K (K (Toplevel.toplevel, [])));
-
-fun context () = Toplevel.context_of (state ())
- handle Toplevel.UNDEF => error "Unknown context";
-
-fun goal () = #2 (#2 (Proof.get_goal (Toplevel.proof_of (state ()))))
- handle Toplevel.UNDEF => error "No goal present";
-
-fun print () = Toplevel.print_state false (state ());
-
-
-(* history navigation *)
-
-local
-
-fun find_and_undo _ [] = error "Undo history exhausted"
- | find_and_undo which ((prev, tr) :: hist) =
- ((case Toplevel.init_of tr of SOME name => ThyInfo.kill_thy name | NONE => ());
- if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist);
-
-in
-
-fun linear_undo n = edit_history n (K (find_and_undo (K true)));
-
-fun undo n = edit_history n (fn st => fn hist =>
- find_and_undo (if Toplevel.is_proof st then K true else OuterKeyword.is_theory) hist);
-
-fun kill () = edit_history 1 (fn st => fn hist =>
- find_and_undo
- (if Toplevel.is_proof st then OuterKeyword.is_theory else OuterKeyword.is_theory_begin) hist);
-
-fun kill_proof () = edit_history 1 (fn st => fn hist =>
- if Toplevel.is_proof st then find_and_undo OuterKeyword.is_theory hist
- else raise Toplevel.UNDEF);
-
-end;
-
-
-(* interactive state transformations *)
-
-fun op >> tr =
- (case Toplevel.transition true tr (state ()) of
- NONE => false
- | SOME (_, SOME err) => (set_exn (SOME err); Toplevel.error_msg tr err; true)
- | SOME (st', NONE) =>
- let
- val name = Toplevel.name_of tr;
- val _ = if OuterKeyword.is_theory_begin name then init () else ();
- val _ =
- if OuterKeyword.is_regular name
- then edit_history 1 (fn st => fn hist => (st', (st, tr) :: hist)) else ();
- in true end);
-
-fun op >>> [] = ()
- | op >>> (tr :: trs) = if op >> tr then op >>> trs else ();
-
-
-(* toplevel loop *)
-
-val crashes = ref ([]: exn list);
-
-local
-
-fun raw_loop secure src =
- let
- fun check_secure () =
- (if secure then warning "Secure loop -- cannot exit to ML" else (); secure);
- in
- (case Source.get_single (Source.set_prompt Source.default_prompt src) of
- NONE => if secure then quit () else ()
- | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
- handle exn =>
- (Output.error_msg (Toplevel.exn_message exn)
- handle crash =>
- (CRITICAL (fn () => change crashes (cons crash));
- warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
- raw_loop secure src)
- end;
-
-in
-
-fun toplevel_loop {init = do_init, welcome, sync, secure} =
- (Context.set_thread_data NONE;
- if do_init then init () else (); (* FIXME init editor model *)
- if welcome then writeln (Session.welcome ()) else ();
- uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ());
-
-end;
-
-fun loop () =
- toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
-
-fun main () =
- toplevel_loop {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};
-
-
-
-(** individual toplevel commands **)
-
-(* unique identification *)
-
-type id = string;
-val no_id : id = "";
-
-
-(* command category *)
-
-datatype category = Empty | Theory | Proof | Diag | Control;
-
-fun category_of tr =
- let val name = Toplevel.name_of tr in
- if name = "" then Empty
- else if OuterKeyword.is_theory name then Theory
- else if OuterKeyword.is_proof name then Proof
- else if OuterKeyword.is_diag name then Diag
- else Control
- end;
-
-val is_theory = fn Theory => true | _ => false;
-val is_proper = fn Theory => true | Proof => true | _ => false;
-val is_regular = fn Control => false | _ => true;
-
-
-(* command status *)
-
-datatype status =
- Unprocessed |
- Running |
- Failed of exn * string |
- Finished of Toplevel.state;
-
-fun status_markup Unprocessed = Markup.unprocessed
- | status_markup Running = (Markup.runningN, [])
- | status_markup (Failed _) = Markup.failed
- | status_markup (Finished _) = Markup.finished;
-
-fun run int tr state =
- (case Toplevel.transition int tr state of
- NONE => NONE
- | SOME (_, SOME err) => (Toplevel.error_msg tr err; SOME (Failed err))
- | SOME (state', NONE) => SOME (Finished state'));
-
-
-(* datatype command *)
-
-datatype command = Command of
- {category: category,
- transition: Toplevel.transition,
- status: status};
-
-fun make_command (category, transition, status) =
- Command {category = category, transition = transition, status = status};
-
-val empty_command =
- make_command (Empty, Toplevel.empty, Finished Toplevel.toplevel);
-
-fun map_command f (Command {category, transition, status}) =
- make_command (f (category, transition, status));
-
-fun map_status f = map_command (fn (category, transition, status) =>
- (category, transition, f status));
-
-
-(* global collection of identified commands *)
-
-fun err_dup id = sys_error ("Duplicate command " ^ quote id);
-fun err_undef id = sys_error ("Unknown command " ^ quote id);
-
-local val global_commands = ref (Graph.empty: command Graph.T) in
-
-fun change_commands f = NAMED_CRITICAL "Isar" (fn () => change global_commands f)
- handle Graph.DUP bad => err_dup bad | Graph.UNDEF bad => err_undef bad;
-
-fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands);
-
-end;
-
-fun add_edge (id1, id2) =
- if id1 = no_id orelse id2 = no_id then I else Graph.add_edge (id1, id2);
-
-
-fun init_commands () = change_commands (K Graph.empty);
-
-fun the_command id =
- let val Command cmd =
- if id = no_id then empty_command
- else (Graph.get_node (get_commands ()) id handle Graph.UNDEF bad => err_undef bad)
- in cmd end;
-
-fun prev_command id =
- if id = no_id then no_id
- else
- (case Graph.imm_preds (get_commands ()) id handle Graph.UNDEF bad => err_undef bad of
- [] => no_id
- | [prev] => prev
- | _ => sys_error ("Non-linear command dependency " ^ quote id));
-
-fun next_commands id =
- if id = no_id then []
- else Graph.imm_succs (get_commands ()) id handle Graph.UNDEF bad => err_undef bad;
-
-fun descendant_commands ids =
- Graph.all_succs (get_commands ()) (distinct (op =) (filter_out (fn id => id = no_id) ids))
- handle Graph.UNDEF bad => err_undef bad;
-
-
-(* maintain status *)
-
-fun report_status markup id = Toplevel.status (#transition (the_command id)) markup;
-
-fun update_status status id = change_commands (Graph.map_node id (map_status (K status)));
-
-fun report_update_status status id =
- change_commands (Graph.map_node id (map_status (fn old_status =>
- let val markup = status_markup status
- in if markup <> status_markup old_status then report_status markup id else (); status end)));
-
-
-(* create and dispose commands *)
-
-fun create_command raw_tr =
- let
- val (id, tr) =
- (case Toplevel.get_id raw_tr of
- SOME id => (id, raw_tr)
- | NONE =>
- let val id =
- if ! Toplevel.debug then "isabelle:" ^ Toplevel.name_of raw_tr ^ serial_string ()
- else "isabelle:" ^ serial_string ()
- in (id, Toplevel.put_id id raw_tr) end);
-
- val cmd = make_command (category_of tr, tr, Unprocessed);
- val _ = change_commands (Graph.new_node (id, cmd));
- in id end;
-
-fun dispose_commands ids =
- let
- val desc = descendant_commands ids;
- val _ = List.app (report_status Markup.disposed) desc;
- val _ = change_commands (Graph.del_nodes desc);
- in () end;
-
-
-(* final state *)
-
-fun the_state id =
- (case the_command id of
- {status = Finished state, ...} => state
- | {transition, ...} => error ("Unfinished command " ^ Toplevel.str_of transition));
-
-
-
-(** editor model **)
-
-(* run commands *)
-
-fun try_run id =
- (case try the_state (prev_command id) of
- NONE => ()
- | SOME state =>
- (case run true (#transition (the_command id)) state of
- NONE => ()
- | SOME status => report_update_status status id));
-
-fun rerun_commands ids =
- (List.app (report_update_status Unprocessed) ids; List.app try_run ids);
-
-
-(* modify document *)
-
-fun insert_command prev id = NAMED_CRITICAL "Isar" (fn () =>
- let
- val nexts = next_commands prev;
- val _ = change_commands
- (fold (fn next => Graph.del_edge (prev, next)) nexts #> add_edge (prev, id) #>
- fold (fn next => Graph.add_edge (id, next)) nexts);
- in descendant_commands [id] end) |> rerun_commands;
-
-fun remove_command id = NAMED_CRITICAL "Isar" (fn () =>
- let
- val prev = prev_command id;
- val nexts = next_commands id;
- val _ = change_commands
- (fold (fn next => Graph.del_edge (id, next)) nexts #>
- fold (fn next => add_edge (prev, next)) nexts);
- in descendant_commands nexts end) |> rerun_commands;
-
-
-(* concrete syntax *)
-
-local
-
-structure P = OuterParse;
-val op >> = Scan.>>;
-
-in
-
-val _ =
- OuterSyntax.internal_command "Isar.command"
- (P.string -- P.string >> (fn (id, text) =>
- Toplevel.imperative (fn () =>
- ignore (create_command (OuterSyntax.prepare_command (Position.id id) text)))));
-
-val _ =
- OuterSyntax.internal_command "Isar.insert"
- (P.string -- P.string >> (fn (prev, id) =>
- Toplevel.imperative (fn () => insert_command prev id)));
-
-val _ =
- OuterSyntax.internal_command "Isar.remove"
- (P.string >> (fn id => Toplevel.imperative (fn () => remove_command id)));
-
-end;
-
-end;
--- a/src/Pure/Isar/isar_cmd.ML Sat Feb 28 17:09:32 2009 +0100
+++ b/src/Pure/Isar/isar_cmd.ML Sat Feb 28 18:00:20 2009 +0100
@@ -32,7 +32,6 @@
val skip_proof: Toplevel.transition -> Toplevel.transition
val init_theory: string * string list * (string * bool) list ->
Toplevel.transition -> Toplevel.transition
- val welcome: Toplevel.transition -> Toplevel.transition
val exit: Toplevel.transition -> Toplevel.transition
val quit: Toplevel.transition -> Toplevel.transition
val pr: string list * (int option * int option) -> Toplevel.transition -> Toplevel.transition
@@ -265,8 +264,6 @@
if ThyInfo.check_known_thy (Context.theory_name thy)
then ThyInfo.end_theory thy else ());
-val welcome = Toplevel.imperative (writeln o Session.welcome);
-
val exit = Toplevel.keep (fn state =>
(Context.set_thread_data (try Toplevel.generic_theory_of state);
raise Toplevel.TERMINATE));
--- a/src/Pure/Isar/isar_syn.ML Sat Feb 28 17:09:32 2009 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sat Feb 28 18:00:20 2009 +0100
@@ -729,39 +729,6 @@
handle ERROR msg => Scan.fail_with (K msg)));
-(* global history commands *)
-
-val _ =
- OuterSyntax.improper_command "init_toplevel" "init toplevel point-of-interest" K.control
- (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.init));
-
-val _ =
- OuterSyntax.improper_command "linear_undo" "undo commands" K.control
- (Scan.optional P.nat 1 >>
- (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.linear_undo n)));
-
-val _ =
- OuterSyntax.improper_command "undo" "undo commands (skipping closed proofs)" K.control
- (Scan.optional P.nat 1 >>
- (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo n)));
-
-val _ =
- OuterSyntax.improper_command "undos_proof" "undo commands (skipping closed proofs)" K.control
- (Scan.optional P.nat 1 >> (fn n => Toplevel.no_timing o
- Toplevel.keep (fn state =>
- if Toplevel.is_proof state then (Isar.undo n; Isar.print ()) else raise Toplevel.UNDEF)));
-
-val _ =
- OuterSyntax.improper_command "cannot_undo" "partial undo -- Proof General legacy" K.control
- (P.name >>
- (fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)
- | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
-
-val _ =
- OuterSyntax.improper_command "kill" "kill partial proof or theory development" K.control
- (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.kill));
-
-
(** diagnostic commands (for interactive mode only) **)
@@ -974,9 +941,5 @@
OuterSyntax.improper_command "exit" "exit Isar loop" K.control
(Scan.succeed (Toplevel.no_timing o IsarCmd.exit));
-val _ =
- OuterSyntax.improper_command "welcome" "print welcome message" K.diag
- (Scan.succeed (Toplevel.no_timing o IsarCmd.welcome));
-
end;
--- a/src/Pure/Isar/session.ML Sat Feb 28 17:09:32 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,105 +0,0 @@
-(* Title: Pure/Isar/session.ML
- Author: Markus Wenzel, TU Muenchen
-
-Session management -- maintain state of logic images.
-*)
-
-signature SESSION =
-sig
- val id: unit -> string list
- val name: unit -> string
- val welcome: unit -> string
- val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool -> string list ->
- string -> string -> bool * string -> string -> int -> bool -> int -> int -> bool -> unit
- val finish: unit -> unit
-end;
-
-structure Session: SESSION =
-struct
-
-
-(* session state *)
-
-val session = ref ([Context.PureN]: string list);
-val session_path = ref ([]: string list);
-val session_finished = ref false;
-val remote_path = ref (NONE: Url.T option);
-
-
-(* access path *)
-
-fun id () = ! session;
-fun path () = ! session_path;
-
-fun str_of [] = Context.PureN
- | str_of elems = space_implode "/" elems;
-
-fun name () = "Isabelle/" ^ str_of (path ());
-
-fun welcome () =
- if Distribution.is_official then
- "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
- else
- "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")" ^
- (if Distribution.changelog <> "" then "\nSee also " ^ Distribution.changelog else "");
-
-
-(* add_path *)
-
-fun add_path reset s =
- let val sess = ! session @ [s] in
- (case duplicates (op =) sess of
- [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
- | dups => error ("Duplicate session identifiers " ^ commas_quote dups ^ " in " ^ str_of sess))
- end;
-
-
-(* init *)
-
-fun init reset parent name =
- if not (member (op =) (! session) parent) 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 () =
- (Output.accumulated_time ();
- ThyInfo.finish ();
- Present.finish ();
- Future.shutdown ();
- session_finished := true);
-
-
-(* use_dir *)
-
-fun get_rpath rpath =
- (if rpath = "" then () else
- if is_some (! remote_path) then
- error "Path for remote theory browsing information may only be set once"
- else
- remote_path := SOME (Url.explode rpath);
- (! remote_path, rpath <> ""));
-
-fun dumping (_, "") = NONE
- | dumping (cp, path) = SOME (cp, Path.explode path);
-
-fun use_dir root build modes reset info doc doc_graph doc_versions
- parent name dump rpath level verbose max_threads trace_threads parallel_proofs =
- ((fn () =>
- (init reset parent name;
- Present.init build info doc doc_graph doc_versions (path ()) name
- (dumping dump) (get_rpath rpath) verbose (map ThyInfo.get_theory (ThyInfo.get_names ()));
- use root;
- finish ()))
- |> setmp_noncritical Proofterm.proofs level
- |> setmp_noncritical print_mode (modes @ print_mode_value ())
- |> setmp_noncritical Goal.parallel_proofs parallel_proofs
- |> setmp_noncritical Multithreading.trace trace_threads
- |> setmp_noncritical Multithreading.max_threads
- (if Multithreading.available then max_threads
- else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
- handle exn => (Output.error_msg (Toplevel.exn_message exn); exit 1);
-
-end;
--- a/src/Pure/ROOT.ML Sat Feb 28 17:09:32 2009 +0100
+++ b/src/Pure/ROOT.ML Sat Feb 28 18:00:20 2009 +0100
@@ -81,12 +81,18 @@
use "goal.ML";
use "axclass.ML";
-(*the main Isar system*)
+(*main Isar stuff*)
cd "Isar"; use "ROOT.ML"; cd "..";
use "subgoal.ML";
use "Proof/extraction.ML";
+(*Isabelle/Isar system*)
+use "System/session.ML";
+use "System/isar.ML";
+use "System/isabelle_process.ML";
+
+(*additional tools*)
cd "Tools"; use "ROOT.ML"; cd "..";
use "codegen.ML";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/isabelle_process.ML Sat Feb 28 18:00:20 2009 +0100
@@ -0,0 +1,138 @@
+(* Title: Pure/System/isabelle_process.ML
+ Author: Makarius
+
+Isabelle process wrapper -- interaction via external program.
+
+General format of process output:
+
+ (1) unmarked stdout/stderr, no line structure (output should be
+ processed immediately as it arrives);
+
+ (2) properly marked-up messages, e.g. for writeln channel
+
+ "\002A" ^ props ^ "\002,\n" ^ text ^ "\002.\n"
+
+ where the props consist of name=value lines terminated by "\002,\n"
+ each, and the remaining text is any number of lines (output is
+ supposed to be processed in one piece);
+
+ (3) special init message holds "pid" and "session" property;
+
+ (4) message content is encoded in YXML format.
+*)
+
+signature ISABELLE_PROCESS =
+sig
+ val isabelle_processN: string
+ val init: string -> unit
+end;
+
+structure IsabelleProcess: ISABELLE_PROCESS =
+struct
+
+(* print modes *)
+
+val isabelle_processN = "isabelle_process";
+
+val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
+val _ = Markup.add_mode isabelle_processN YXML.output_markup;
+
+
+(* message markup *)
+
+fun special ch = Symbol.STX ^ ch;
+val special_sep = special ",";
+val special_end = special ".";
+
+local
+
+fun clean_string bad str =
+ if exists_string (member (op =) bad) str then
+ translate_string (fn c => if member (op =) bad c then Symbol.DEL else c) str
+ else str;
+
+fun message_props props =
+ let val clean = clean_string [Symbol.STX, "\n", "\r"]
+ in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end;
+
+fun message_pos trees = trees |> get_first
+ (fn XML.Elem (name, atts, ts) =>
+ if name = Markup.positionN then SOME (Position.of_properties atts)
+ else message_pos ts
+ | _ => NONE);
+
+fun output out_stream s = NAMED_CRITICAL "IO" (fn () =>
+ (TextIO.output (out_stream, s); TextIO.output (out_stream, "\n")));
+
+in
+
+fun message _ _ "" = ()
+ | message out_stream ch body =
+ let
+ val pos = the_default Position.none (message_pos (YXML.parse_body body));
+ val props =
+ Position.properties_of (Position.thread_data ())
+ |> Position.default_properties pos;
+ val txt = clean_string [Symbol.STX] body;
+ in output out_stream (special ch ^ message_props props ^ txt ^ special_end) end;
+
+fun init_message out_stream =
+ let
+ val pid = (Markup.pidN, process_id ());
+ val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown");
+ val text = Session.welcome ();
+ in output out_stream (special "A" ^ message_props [pid, session] ^ text ^ special_end) end;
+
+end;
+
+
+(* channels *)
+
+local
+
+fun auto_flush stream =
+ let
+ val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream stream, IO.BLOCK_BUF);
+ fun loop () =
+ (OS.Process.sleep (Time.fromMilliseconds 50); try TextIO.flushOut stream; loop ());
+ in loop end;
+
+in
+
+fun setup_channels out =
+ let
+ val out_stream =
+ if out = "-" then TextIO.stdOut
+ else
+ let
+ val path = File.platform_path (Path.explode out);
+ val out_stream = TextIO.openOut path; (*fifo blocks until reader is ready*)
+ val _ = OS.FileSys.remove path; (*prevent alien access, indicate writer is ready*)
+ val _ = SimpleThread.fork false (auto_flush TextIO.stdOut);
+ in out_stream end;
+ val _ = SimpleThread.fork false (auto_flush out_stream);
+ val _ = SimpleThread.fork false (auto_flush TextIO.stdErr);
+ in
+ Output.status_fn := message out_stream "B";
+ Output.writeln_fn := message out_stream "C";
+ Output.priority_fn := message out_stream "D";
+ Output.tracing_fn := message out_stream "E";
+ Output.warning_fn := message out_stream "F";
+ Output.error_fn := message out_stream "G";
+ Output.debug_fn := message out_stream "H";
+ Output.prompt_fn := ignore;
+ out_stream
+ end;
+
+end;
+
+
+(* init *)
+
+fun init out =
+ (change print_mode (update (op =) isabelle_processN);
+ setup_channels out |> init_message;
+ OuterKeyword.report ();
+ Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/isabelle_process.scala Sat Feb 28 18:00:20 2009 +0100
@@ -0,0 +1,435 @@
+/* Title: Pure/System/isabelle_process.ML
+ Author: Makarius
+ Options: :folding=explicit:collapseFolds=1:
+
+Isabelle process management -- always reactive due to multi-threaded I/O.
+*/
+
+package isabelle
+
+import java.util.concurrent.LinkedBlockingQueue
+import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
+ InputStream, OutputStream, IOException}
+
+
+object IsabelleProcess {
+
+ /* results */
+
+ object Kind extends Enumeration {
+ //{{{ values and codes
+ // internal system notification
+ val SYSTEM = Value("SYSTEM")
+ // Posix channels/events
+ val STDIN = Value("STDIN")
+ val STDOUT = Value("STDOUT")
+ val SIGNAL = Value("SIGNAL")
+ val EXIT = Value("EXIT")
+ // Isabelle messages
+ val INIT = Value("INIT")
+ val STATUS = Value("STATUS")
+ val WRITELN = Value("WRITELN")
+ val PRIORITY = Value("PRIORITY")
+ val TRACING = Value("TRACING")
+ val WARNING = Value("WARNING")
+ val ERROR = Value("ERROR")
+ val DEBUG = Value("DEBUG")
+ // messages codes
+ val code = Map(
+ ('A' : Int) -> Kind.INIT,
+ ('B' : Int) -> Kind.STATUS,
+ ('C' : Int) -> Kind.WRITELN,
+ ('D' : Int) -> Kind.PRIORITY,
+ ('E' : Int) -> Kind.TRACING,
+ ('F' : Int) -> Kind.WARNING,
+ ('G' : Int) -> Kind.ERROR,
+ ('H' : Int) -> Kind.DEBUG,
+ ('0' : Int) -> Kind.SYSTEM,
+ ('1' : Int) -> Kind.STDIN,
+ ('2' : Int) -> Kind.STDOUT,
+ ('3' : Int) -> Kind.SIGNAL,
+ ('4' : Int) -> Kind.EXIT)
+ // message markup
+ val markup = Map(
+ Kind.INIT -> Markup.INIT,
+ Kind.STATUS -> Markup.STATUS,
+ Kind.WRITELN -> Markup.WRITELN,
+ Kind.PRIORITY -> Markup.PRIORITY,
+ Kind.TRACING -> Markup.TRACING,
+ Kind.WARNING -> Markup.WARNING,
+ Kind.ERROR -> Markup.ERROR,
+ Kind.DEBUG -> Markup.DEBUG,
+ Kind.SYSTEM -> Markup.SYSTEM,
+ Kind.STDIN -> Markup.STDIN,
+ Kind.STDOUT -> Markup.STDOUT,
+ Kind.SIGNAL -> Markup.SIGNAL,
+ Kind.EXIT -> Markup.EXIT)
+ //}}}
+ def is_raw(kind: Value) =
+ kind == STDOUT
+ def is_control(kind: Value) =
+ kind == SYSTEM ||
+ kind == SIGNAL ||
+ kind == EXIT
+ def is_system(kind: Value) =
+ kind == SYSTEM ||
+ kind == STDIN ||
+ kind == SIGNAL ||
+ kind == EXIT ||
+ kind == STATUS
+ }
+
+ class Result(val kind: Kind.Value, val props: List[(String, String)], val result: String) {
+ override def toString = {
+ val trees = YXML.parse_body_failsafe(result)
+ val res =
+ if (kind == Kind.STATUS) trees.map(_.toString).mkString
+ else trees.flatMap(XML.content(_).mkString).mkString
+ if (props.isEmpty)
+ kind.toString + " [[" + res + "]]"
+ else
+ kind.toString + " " +
+ (for ((x, y) <- props) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
+ }
+ def is_raw = Kind.is_raw(kind)
+ def is_control = Kind.is_control(kind)
+ def is_system = Kind.is_system(kind)
+ }
+
+ def parse_message(isabelle_system: IsabelleSystem, result: Result) =
+ {
+ XML.Elem(Markup.MESSAGE, (Markup.CLASS, Kind.markup(result.kind)) :: result.props,
+ YXML.parse_body_failsafe(isabelle_system.symbols.decode(result.result)))
+ }
+}
+
+
+class IsabelleProcess(isabelle_system: IsabelleSystem,
+ results: EventBus[IsabelleProcess.Result], args: String*)
+{
+ import IsabelleProcess._
+
+
+ /* demo constructor */
+
+ def this(args: String*) =
+ this(new IsabelleSystem, new EventBus[IsabelleProcess.Result] + Console.println, args: _*)
+
+
+ /* process information */
+
+ @volatile private var proc: Process = null
+ @volatile private var closing = false
+ @volatile private var pid: String = null
+ @volatile private var the_session: String = null
+ def session = the_session
+
+
+ /* results */
+
+ def parse_message(result: Result): XML.Tree =
+ IsabelleProcess.parse_message(isabelle_system, result)
+
+ private val result_queue = new LinkedBlockingQueue[Result]
+
+ private def put_result(kind: Kind.Value, props: List[(String, String)], result: String)
+ {
+ if (kind == Kind.INIT) {
+ val map = Map(props: _*)
+ if (map.isDefinedAt(Markup.PID)) pid = map(Markup.PID)
+ if (map.isDefinedAt(Markup.SESSION)) the_session = map(Markup.SESSION)
+ }
+ result_queue.put(new Result(kind, props, result))
+ }
+
+ private class ResultThread extends Thread("isabelle: results") {
+ override def run() = {
+ var finished = false
+ while (!finished) {
+ val result =
+ try { result_queue.take }
+ catch { case _: NullPointerException => null }
+
+ if (result != null) {
+ results.event(result)
+ if (result.kind == Kind.EXIT) finished = true
+ }
+ else finished = true
+ }
+ }
+ }
+
+
+ /* signals */
+
+ def interrupt() = synchronized {
+ if (proc == null) error("Cannot interrupt Isabelle: no process")
+ if (pid == null) put_result(Kind.SYSTEM, Nil, "Cannot interrupt: unknown pid")
+ else {
+ try {
+ if (isabelle_system.execute(true, "kill", "-INT", pid).waitFor == 0)
+ put_result(Kind.SIGNAL, Nil, "INT")
+ else
+ put_result(Kind.SYSTEM, Nil, "Cannot interrupt: kill command failed")
+ }
+ catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
+ }
+ }
+
+ def kill() = synchronized {
+ if (proc == 0) error("Cannot kill Isabelle: no process")
+ else {
+ try_close()
+ Thread.sleep(500)
+ put_result(Kind.SIGNAL, Nil, "KILL")
+ proc.destroy
+ proc = null
+ pid = null
+ }
+ }
+
+
+ /* output being piped into the process */
+
+ private val output = new LinkedBlockingQueue[String]
+
+ private def output_raw(text: String) = synchronized {
+ if (proc == null) error("Cannot output to Isabelle: no process")
+ if (closing) error("Cannot output to Isabelle: already closing")
+ output.put(text)
+ }
+
+ def output_sync(text: String) =
+ output_raw(" \\<^sync>\n; " + text + " \\<^sync>;\n")
+
+
+ def command(text: String) =
+ output_sync("Isabelle.command " + IsabelleSyntax.encode_string(text))
+
+ def command(props: List[(String, String)], text: String) =
+ output_sync("Isabelle.command " + IsabelleSyntax.encode_properties(props) + " " +
+ IsabelleSyntax.encode_string(text))
+
+ def ML(text: String) =
+ output_sync("ML_val " + IsabelleSyntax.encode_string(text))
+
+ def close() = synchronized { // FIXME watchdog/timeout
+ output_raw("\u0000")
+ closing = true
+ }
+
+ def try_close() = synchronized {
+ if (proc != null && !closing) {
+ try { close() }
+ catch { case _: RuntimeException => }
+ }
+ }
+
+
+ /* stdin */
+
+ private class StdinThread(out_stream: OutputStream) extends Thread("isabelle: stdin") {
+ override def run() = {
+ val writer = new BufferedWriter(new OutputStreamWriter(out_stream, isabelle_system.charset))
+ var finished = false
+ while (!finished) {
+ try {
+ //{{{
+ val s = output.take
+ if (s == "\u0000") {
+ writer.close
+ finished = true
+ }
+ else {
+ put_result(Kind.STDIN, Nil, s)
+ writer.write(s)
+ writer.flush
+ }
+ //}}}
+ }
+ catch {
+ case e: IOException => put_result(Kind.SYSTEM, Nil, "Stdin thread: " + e.getMessage)
+ }
+ }
+ put_result(Kind.SYSTEM, Nil, "Stdin thread terminated")
+ }
+ }
+
+
+ /* stdout */
+
+ private class StdoutThread(in_stream: InputStream) extends Thread("isabelle: stdout") {
+ override def run() = {
+ val reader = new BufferedReader(new InputStreamReader(in_stream, isabelle_system.charset))
+ var result = new StringBuilder(100)
+
+ var finished = false
+ while (!finished) {
+ try {
+ //{{{
+ var c = -1
+ var done = false
+ while (!done && (result.length == 0 || reader.ready)) {
+ c = reader.read
+ if (c >= 0) result.append(c.asInstanceOf[Char])
+ else done = true
+ }
+ if (result.length > 0) {
+ put_result(Kind.STDOUT, Nil, result.toString)
+ result.length = 0
+ }
+ else {
+ reader.close
+ finished = true
+ try_close()
+ }
+ //}}}
+ }
+ catch {
+ case e: IOException => put_result(Kind.SYSTEM, Nil, "Stdout thread: " + e.getMessage)
+ }
+ }
+ put_result(Kind.SYSTEM, Nil, "Stdout thread terminated")
+ }
+ }
+
+
+ /* messages */
+
+ private class MessageThread(fifo: String) extends Thread("isabelle: messages") {
+ override def run() = {
+ val reader = isabelle_system.fifo_reader(fifo)
+ var kind: Kind.Value = null
+ var props: List[(String, String)] = Nil
+ var result = new StringBuilder
+
+ var finished = false
+ while (!finished) {
+ try {
+ if (kind == null) {
+ //{{{ Char mode -- resync
+ var c = -1
+ do {
+ c = reader.read
+ if (c >= 0 && c != 2) result.append(c.asInstanceOf[Char])
+ } while (c >= 0 && c != 2)
+
+ if (result.length > 0) {
+ put_result(Kind.SYSTEM, Nil, "Malformed message:\n" + result.toString)
+ result.length = 0
+ }
+ if (c < 0) {
+ reader.close
+ finished = true
+ try_close()
+ }
+ else {
+ c = reader.read
+ if (Kind.code.isDefinedAt(c)) kind = Kind.code(c)
+ else kind = null
+ }
+ //}}}
+ }
+ else {
+ //{{{ Line mode
+ val line = reader.readLine
+ if (line == null) {
+ reader.close
+ finished = true
+ try_close()
+ }
+ else {
+ val len = line.length
+ // property
+ if (line.endsWith("\u0002,")) {
+ val i = line.indexOf('=')
+ if (i > 0) {
+ val name = line.substring(0, i)
+ val value = line.substring(i + 1, len - 2)
+ props = (name, value) :: props
+ }
+ }
+ // last text line
+ else if (line.endsWith("\u0002.")) {
+ result.append(line.substring(0, len - 2))
+ put_result(kind, props.reverse, result.toString)
+ kind = null
+ props = Nil
+ result.length = 0
+ }
+ // text line
+ else {
+ result.append(line)
+ result.append('\n')
+ }
+ }
+ //}}}
+ }
+ }
+ catch {
+ case e: IOException => put_result(Kind.SYSTEM, Nil, "Message thread: " + e.getMessage)
+ }
+ }
+ put_result(Kind.SYSTEM, Nil, "Message thread terminated")
+ }
+ }
+
+
+
+ /** main **/
+
+ {
+ /* isabelle version */
+
+ {
+ val (msg, rc) = isabelle_system.isabelle_tool("version")
+ if (rc != 0) error("Version check failed -- bad Isabelle installation:\n" + msg)
+ put_result(Kind.SYSTEM, Nil, msg)
+ }
+
+
+ /* messages */
+
+ val message_fifo = isabelle_system.mk_fifo()
+ def rm_fifo() = isabelle_system.rm_fifo(message_fifo)
+
+ val message_thread = new MessageThread(message_fifo)
+ message_thread.start
+
+ new ResultThread().start
+
+
+ /* exec process */
+
+ try {
+ val cmdline =
+ List(isabelle_system.getenv_strict("ISABELLE_PROCESS"), "-W", message_fifo) ++ args
+ proc = isabelle_system.execute(true, cmdline: _*)
+ }
+ catch {
+ case e: IOException =>
+ rm_fifo()
+ error("Failed to execute Isabelle process: " + e.getMessage)
+ }
+
+
+ /* stdin/stdout */
+
+ new StdinThread(proc.getOutputStream).start
+ new StdoutThread(proc.getInputStream).start
+
+
+ /* exit */
+
+ new Thread("isabelle: exit") {
+ override def run() = {
+ val rc = proc.waitFor()
+ Thread.sleep(300)
+ put_result(Kind.SYSTEM, Nil, "Exit thread terminated")
+ put_result(Kind.EXIT, Nil, Integer.toString(rc))
+ rm_fifo()
+ }
+ }.start
+
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/isar.ML Sat Feb 28 18:00:20 2009 +0100
@@ -0,0 +1,415 @@
+(* Title: Pure/Isar/isar.ML
+ Author: Makarius
+
+The global Isabelle/Isar state and main read-eval-print loop.
+*)
+
+signature ISAR =
+sig
+ val init: unit -> unit
+ val exn: unit -> (exn * string) option
+ val state: unit -> Toplevel.state
+ val context: unit -> Proof.context
+ val goal: unit -> thm
+ val print: unit -> unit
+ val >> : Toplevel.transition -> bool
+ val >>> : Toplevel.transition list -> unit
+ val linear_undo: int -> unit
+ val undo: int -> unit
+ val kill: unit -> unit
+ val kill_proof: unit -> unit
+ val crashes: exn list ref
+ val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
+ val loop: unit -> unit
+ val main: unit -> unit
+
+ type id = string
+ val no_id: id
+ val create_command: Toplevel.transition -> id
+ val insert_command: id -> id -> unit
+ val remove_command: id -> unit
+end;
+
+structure Isar: ISAR =
+struct
+
+
+(** TTY model -- SINGLE-THREADED! **)
+
+(* the global state *)
+
+type history = (Toplevel.state * Toplevel.transition) list;
+ (*previous state, state transition -- regular commands only*)
+
+local
+ val global_history = ref ([]: history);
+ val global_state = ref Toplevel.toplevel;
+ val global_exn = ref (NONE: (exn * string) option);
+in
+
+fun edit_history count f = NAMED_CRITICAL "Isar" (fn () =>
+ let
+ fun edit 0 (st, hist) = (global_history := hist; global_state := st; global_exn := NONE)
+ | edit n (st, hist) = edit (n - 1) (f st hist);
+ in edit count (! global_state, ! global_history) end);
+
+fun state () = NAMED_CRITICAL "Isar" (fn () => ! global_state);
+fun set_state state = NAMED_CRITICAL "Isar" (fn () => global_state := state);
+
+fun exn () = NAMED_CRITICAL "Isar" (fn () => ! global_exn);
+fun set_exn exn = NAMED_CRITICAL "Isar" (fn () => global_exn := exn);
+
+end;
+
+
+fun init () = edit_history 1 (K (K (Toplevel.toplevel, [])));
+
+fun context () = Toplevel.context_of (state ())
+ handle Toplevel.UNDEF => error "Unknown context";
+
+fun goal () = #2 (#2 (Proof.get_goal (Toplevel.proof_of (state ()))))
+ handle Toplevel.UNDEF => error "No goal present";
+
+fun print () = Toplevel.print_state false (state ());
+
+
+(* history navigation *)
+
+local
+
+fun find_and_undo _ [] = error "Undo history exhausted"
+ | find_and_undo which ((prev, tr) :: hist) =
+ ((case Toplevel.init_of tr of SOME name => ThyInfo.kill_thy name | NONE => ());
+ if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist);
+
+in
+
+fun linear_undo n = edit_history n (K (find_and_undo (K true)));
+
+fun undo n = edit_history n (fn st => fn hist =>
+ find_and_undo (if Toplevel.is_proof st then K true else OuterKeyword.is_theory) hist);
+
+fun kill () = edit_history 1 (fn st => fn hist =>
+ find_and_undo
+ (if Toplevel.is_proof st then OuterKeyword.is_theory else OuterKeyword.is_theory_begin) hist);
+
+fun kill_proof () = edit_history 1 (fn st => fn hist =>
+ if Toplevel.is_proof st then find_and_undo OuterKeyword.is_theory hist
+ else raise Toplevel.UNDEF);
+
+end;
+
+
+(* interactive state transformations *)
+
+fun op >> tr =
+ (case Toplevel.transition true tr (state ()) of
+ NONE => false
+ | SOME (_, SOME err) => (set_exn (SOME err); Toplevel.error_msg tr err; true)
+ | SOME (st', NONE) =>
+ let
+ val name = Toplevel.name_of tr;
+ val _ = if OuterKeyword.is_theory_begin name then init () else ();
+ val _ =
+ if OuterKeyword.is_regular name
+ then edit_history 1 (fn st => fn hist => (st', (st, tr) :: hist)) else ();
+ in true end);
+
+fun op >>> [] = ()
+ | op >>> (tr :: trs) = if op >> tr then op >>> trs else ();
+
+
+(* toplevel loop *)
+
+val crashes = ref ([]: exn list);
+
+local
+
+fun raw_loop secure src =
+ let
+ fun check_secure () =
+ (if secure then warning "Secure loop -- cannot exit to ML" else (); secure);
+ in
+ (case Source.get_single (Source.set_prompt Source.default_prompt src) of
+ NONE => if secure then quit () else ()
+ | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
+ handle exn =>
+ (Output.error_msg (Toplevel.exn_message exn)
+ handle crash =>
+ (CRITICAL (fn () => change crashes (cons crash));
+ warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
+ raw_loop secure src)
+ end;
+
+in
+
+fun toplevel_loop {init = do_init, welcome, sync, secure} =
+ (Context.set_thread_data NONE;
+ if do_init then init () else (); (* FIXME init editor model *)
+ if welcome then writeln (Session.welcome ()) else ();
+ uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ());
+
+end;
+
+fun loop () =
+ toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
+
+fun main () =
+ toplevel_loop {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};
+
+
+
+(** individual toplevel commands **)
+
+(* unique identification *)
+
+type id = string;
+val no_id : id = "";
+
+
+(* command category *)
+
+datatype category = Empty | Theory | Proof | Diag | Control;
+
+fun category_of tr =
+ let val name = Toplevel.name_of tr in
+ if name = "" then Empty
+ else if OuterKeyword.is_theory name then Theory
+ else if OuterKeyword.is_proof name then Proof
+ else if OuterKeyword.is_diag name then Diag
+ else Control
+ end;
+
+val is_theory = fn Theory => true | _ => false;
+val is_proper = fn Theory => true | Proof => true | _ => false;
+val is_regular = fn Control => false | _ => true;
+
+
+(* command status *)
+
+datatype status =
+ Unprocessed |
+ Running |
+ Failed of exn * string |
+ Finished of Toplevel.state;
+
+fun status_markup Unprocessed = Markup.unprocessed
+ | status_markup Running = (Markup.runningN, [])
+ | status_markup (Failed _) = Markup.failed
+ | status_markup (Finished _) = Markup.finished;
+
+fun run int tr state =
+ (case Toplevel.transition int tr state of
+ NONE => NONE
+ | SOME (_, SOME err) => (Toplevel.error_msg tr err; SOME (Failed err))
+ | SOME (state', NONE) => SOME (Finished state'));
+
+
+(* datatype command *)
+
+datatype command = Command of
+ {category: category,
+ transition: Toplevel.transition,
+ status: status};
+
+fun make_command (category, transition, status) =
+ Command {category = category, transition = transition, status = status};
+
+val empty_command =
+ make_command (Empty, Toplevel.empty, Finished Toplevel.toplevel);
+
+fun map_command f (Command {category, transition, status}) =
+ make_command (f (category, transition, status));
+
+fun map_status f = map_command (fn (category, transition, status) =>
+ (category, transition, f status));
+
+
+(* global collection of identified commands *)
+
+fun err_dup id = sys_error ("Duplicate command " ^ quote id);
+fun err_undef id = sys_error ("Unknown command " ^ quote id);
+
+local val global_commands = ref (Graph.empty: command Graph.T) in
+
+fun change_commands f = NAMED_CRITICAL "Isar" (fn () => change global_commands f)
+ handle Graph.DUP bad => err_dup bad | Graph.UNDEF bad => err_undef bad;
+
+fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands);
+
+end;
+
+fun add_edge (id1, id2) =
+ if id1 = no_id orelse id2 = no_id then I else Graph.add_edge (id1, id2);
+
+
+fun init_commands () = change_commands (K Graph.empty);
+
+fun the_command id =
+ let val Command cmd =
+ if id = no_id then empty_command
+ else (Graph.get_node (get_commands ()) id handle Graph.UNDEF bad => err_undef bad)
+ in cmd end;
+
+fun prev_command id =
+ if id = no_id then no_id
+ else
+ (case Graph.imm_preds (get_commands ()) id handle Graph.UNDEF bad => err_undef bad of
+ [] => no_id
+ | [prev] => prev
+ | _ => sys_error ("Non-linear command dependency " ^ quote id));
+
+fun next_commands id =
+ if id = no_id then []
+ else Graph.imm_succs (get_commands ()) id handle Graph.UNDEF bad => err_undef bad;
+
+fun descendant_commands ids =
+ Graph.all_succs (get_commands ()) (distinct (op =) (filter_out (fn id => id = no_id) ids))
+ handle Graph.UNDEF bad => err_undef bad;
+
+
+(* maintain status *)
+
+fun report_status markup id = Toplevel.status (#transition (the_command id)) markup;
+
+fun update_status status id = change_commands (Graph.map_node id (map_status (K status)));
+
+fun report_update_status status id =
+ change_commands (Graph.map_node id (map_status (fn old_status =>
+ let val markup = status_markup status
+ in if markup <> status_markup old_status then report_status markup id else (); status end)));
+
+
+(* create and dispose commands *)
+
+fun create_command raw_tr =
+ let
+ val (id, tr) =
+ (case Toplevel.get_id raw_tr of
+ SOME id => (id, raw_tr)
+ | NONE =>
+ let val id =
+ if ! Toplevel.debug then "isabelle:" ^ Toplevel.name_of raw_tr ^ serial_string ()
+ else "isabelle:" ^ serial_string ()
+ in (id, Toplevel.put_id id raw_tr) end);
+
+ val cmd = make_command (category_of tr, tr, Unprocessed);
+ val _ = change_commands (Graph.new_node (id, cmd));
+ in id end;
+
+fun dispose_commands ids =
+ let
+ val desc = descendant_commands ids;
+ val _ = List.app (report_status Markup.disposed) desc;
+ val _ = change_commands (Graph.del_nodes desc);
+ in () end;
+
+
+(* final state *)
+
+fun the_state id =
+ (case the_command id of
+ {status = Finished state, ...} => state
+ | {transition, ...} => error ("Unfinished command " ^ Toplevel.str_of transition));
+
+
+
+(** editor model **)
+
+(* run commands *)
+
+fun try_run id =
+ (case try the_state (prev_command id) of
+ NONE => ()
+ | SOME state =>
+ (case run true (#transition (the_command id)) state of
+ NONE => ()
+ | SOME status => report_update_status status id));
+
+fun rerun_commands ids =
+ (List.app (report_update_status Unprocessed) ids; List.app try_run ids);
+
+
+(* modify document *)
+
+fun insert_command prev id = NAMED_CRITICAL "Isar" (fn () =>
+ let
+ val nexts = next_commands prev;
+ val _ = change_commands
+ (fold (fn next => Graph.del_edge (prev, next)) nexts #> add_edge (prev, id) #>
+ fold (fn next => Graph.add_edge (id, next)) nexts);
+ in descendant_commands [id] end) |> rerun_commands;
+
+fun remove_command id = NAMED_CRITICAL "Isar" (fn () =>
+ let
+ val prev = prev_command id;
+ val nexts = next_commands id;
+ val _ = change_commands
+ (fold (fn next => Graph.del_edge (id, next)) nexts #>
+ fold (fn next => add_edge (prev, next)) nexts);
+ in descendant_commands nexts end) |> rerun_commands;
+
+
+
+(** command syntax **)
+
+local
+
+structure P = OuterParse and K = OuterKeyword;
+val op >> = Scan.>>;
+
+in
+
+(* global history *)
+
+val _ =
+ OuterSyntax.improper_command "init_toplevel" "init toplevel point-of-interest" K.control
+ (Scan.succeed (Toplevel.no_timing o Toplevel.imperative init));
+
+val _ =
+ OuterSyntax.improper_command "linear_undo" "undo commands" K.control
+ (Scan.optional P.nat 1 >>
+ (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => linear_undo n)));
+
+val _ =
+ OuterSyntax.improper_command "undo" "undo commands (skipping closed proofs)" K.control
+ (Scan.optional P.nat 1 >>
+ (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => undo n)));
+
+val _ =
+ OuterSyntax.improper_command "undos_proof" "undo commands (skipping closed proofs)" K.control
+ (Scan.optional P.nat 1 >> (fn n => Toplevel.no_timing o
+ Toplevel.keep (fn state =>
+ if Toplevel.is_proof state then (undo n; print ()) else raise Toplevel.UNDEF)));
+
+val _ =
+ OuterSyntax.improper_command "cannot_undo" "partial undo -- Proof General legacy" K.control
+ (P.name >>
+ (fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => undo 1)
+ | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
+
+val _ =
+ OuterSyntax.improper_command "kill" "kill partial proof or theory development" K.control
+ (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
+
+
+(* editor model *)
+
+val _ =
+ OuterSyntax.internal_command "Isar.command"
+ (P.string -- P.string >> (fn (id, text) =>
+ Toplevel.imperative (fn () =>
+ ignore (create_command (OuterSyntax.prepare_command (Position.id id) text)))));
+
+val _ =
+ OuterSyntax.internal_command "Isar.insert"
+ (P.string -- P.string >> (fn (prev, id) =>
+ Toplevel.imperative (fn () => insert_command prev id)));
+
+val _ =
+ OuterSyntax.internal_command "Isar.remove"
+ (P.string >> (fn id => Toplevel.imperative (fn () => remove_command id)));
+
+end;
+
+end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/session.ML Sat Feb 28 18:00:20 2009 +0100
@@ -0,0 +1,112 @@
+(* Title: Pure/System/session.ML
+ Author: Markus Wenzel, TU Muenchen
+
+Session management -- maintain state of logic images.
+*)
+
+signature SESSION =
+sig
+ val id: unit -> string list
+ val name: unit -> string
+ val welcome: unit -> string
+ val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool -> string list ->
+ string -> string -> bool * string -> string -> int -> bool -> int -> int -> bool -> unit
+ val finish: unit -> unit
+end;
+
+structure Session: SESSION =
+struct
+
+
+(* session state *)
+
+val session = ref ([Context.PureN]: string list);
+val session_path = ref ([]: string list);
+val session_finished = ref false;
+val remote_path = ref (NONE: Url.T option);
+
+
+(* access path *)
+
+fun id () = ! session;
+fun path () = ! session_path;
+
+fun str_of [] = Context.PureN
+ | str_of elems = space_implode "/" elems;
+
+fun name () = "Isabelle/" ^ str_of (path ());
+
+
+(* welcome *)
+
+fun welcome () =
+ if Distribution.is_official then
+ "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
+ else
+ "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")" ^
+ (if Distribution.changelog <> "" then "\nSee also " ^ Distribution.changelog else "");
+
+val _ =
+ OuterSyntax.improper_command "welcome" "print welcome message" OuterKeyword.diag
+ (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (writeln o welcome)));
+
+
+(* add_path *)
+
+fun add_path reset s =
+ let val sess = ! session @ [s] in
+ (case duplicates (op =) sess of
+ [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
+ | dups => error ("Duplicate session identifiers " ^ commas_quote dups ^ " in " ^ str_of sess))
+ end;
+
+
+(* init *)
+
+fun init reset parent name =
+ if not (member (op =) (! session) parent) 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 () =
+ (Output.accumulated_time ();
+ ThyInfo.finish ();
+ Present.finish ();
+ Future.shutdown ();
+ session_finished := true);
+
+
+(* use_dir *)
+
+fun get_rpath rpath =
+ (if rpath = "" then () else
+ if is_some (! remote_path) then
+ error "Path for remote theory browsing information may only be set once"
+ else
+ remote_path := SOME (Url.explode rpath);
+ (! remote_path, rpath <> ""));
+
+fun dumping (_, "") = NONE
+ | dumping (cp, path) = SOME (cp, Path.explode path);
+
+fun use_dir root build modes reset info doc doc_graph doc_versions
+ parent name dump rpath level verbose max_threads trace_threads parallel_proofs =
+ ((fn () =>
+ (init reset parent name;
+ Present.init build info doc doc_graph doc_versions (path ()) name
+ (dumping dump) (get_rpath rpath) verbose (map ThyInfo.get_theory (ThyInfo.get_names ()));
+ use root;
+ finish ()))
+ |> setmp_noncritical Proofterm.proofs level
+ |> setmp_noncritical print_mode (modes @ print_mode_value ())
+ |> setmp_noncritical Goal.parallel_proofs parallel_proofs
+ |> setmp_noncritical Multithreading.trace trace_threads
+ |> setmp_noncritical Multithreading.max_threads
+ (if Multithreading.available then max_threads
+ else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
+ handle exn => (Output.error_msg (Toplevel.exn_message exn); exit 1);
+
+end;
--- a/src/Pure/Tools/ROOT.ML Sat Feb 28 17:09:32 2009 +0100
+++ b/src/Pure/Tools/ROOT.ML Sat Feb 28 18:00:20 2009 +0100
@@ -4,7 +4,6 @@
*)
use "named_thms.ML";
-use "isabelle_process.ML";
(*basic XML support*)
use "xml_syntax.ML";
--- a/src/Pure/Tools/isabelle_process.ML Sat Feb 28 17:09:32 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,138 +0,0 @@
-(* Title: Pure/Tools/isabelle_process.ML
- Author: Makarius
-
-Isabelle process wrapper -- interaction via external program.
-
-General format of process output:
-
- (1) unmarked stdout/stderr, no line structure (output should be
- processed immediately as it arrives);
-
- (2) properly marked-up messages, e.g. for writeln channel
-
- "\002A" ^ props ^ "\002,\n" ^ text ^ "\002.\n"
-
- where the props consist of name=value lines terminated by "\002,\n"
- each, and the remaining text is any number of lines (output is
- supposed to be processed in one piece);
-
- (3) special init message holds "pid" and "session" property;
-
- (4) message content is encoded in YXML format.
-*)
-
-signature ISABELLE_PROCESS =
-sig
- val isabelle_processN: string
- val init: string -> unit
-end;
-
-structure IsabelleProcess: ISABELLE_PROCESS =
-struct
-
-(* print modes *)
-
-val isabelle_processN = "isabelle_process";
-
-val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
-val _ = Markup.add_mode isabelle_processN YXML.output_markup;
-
-
-(* message markup *)
-
-fun special ch = Symbol.STX ^ ch;
-val special_sep = special ",";
-val special_end = special ".";
-
-local
-
-fun clean_string bad str =
- if exists_string (member (op =) bad) str then
- translate_string (fn c => if member (op =) bad c then Symbol.DEL else c) str
- else str;
-
-fun message_props props =
- let val clean = clean_string [Symbol.STX, "\n", "\r"]
- in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end;
-
-fun message_pos trees = trees |> get_first
- (fn XML.Elem (name, atts, ts) =>
- if name = Markup.positionN then SOME (Position.of_properties atts)
- else message_pos ts
- | _ => NONE);
-
-fun output out_stream s = NAMED_CRITICAL "IO" (fn () =>
- (TextIO.output (out_stream, s); TextIO.output (out_stream, "\n")));
-
-in
-
-fun message _ _ "" = ()
- | message out_stream ch body =
- let
- val pos = the_default Position.none (message_pos (YXML.parse_body body));
- val props =
- Position.properties_of (Position.thread_data ())
- |> Position.default_properties pos;
- val txt = clean_string [Symbol.STX] body;
- in output out_stream (special ch ^ message_props props ^ txt ^ special_end) end;
-
-fun init_message out_stream =
- let
- val pid = (Markup.pidN, process_id ());
- val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown");
- val text = Session.welcome ();
- in output out_stream (special "A" ^ message_props [pid, session] ^ text ^ special_end) end;
-
-end;
-
-
-(* channels *)
-
-local
-
-fun auto_flush stream =
- let
- val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream stream, IO.BLOCK_BUF);
- fun loop () =
- (OS.Process.sleep (Time.fromMilliseconds 50); try TextIO.flushOut stream; loop ());
- in loop end;
-
-in
-
-fun setup_channels out =
- let
- val out_stream =
- if out = "-" then TextIO.stdOut
- else
- let
- val path = File.platform_path (Path.explode out);
- val out_stream = TextIO.openOut path; (*fifo blocks until reader is ready*)
- val _ = OS.FileSys.remove path; (*prevent alien access, indicate writer is ready*)
- val _ = SimpleThread.fork false (auto_flush TextIO.stdOut);
- in out_stream end;
- val _ = SimpleThread.fork false (auto_flush out_stream);
- val _ = SimpleThread.fork false (auto_flush TextIO.stdErr);
- in
- Output.status_fn := message out_stream "B";
- Output.writeln_fn := message out_stream "C";
- Output.priority_fn := message out_stream "D";
- Output.tracing_fn := message out_stream "E";
- Output.warning_fn := message out_stream "F";
- Output.error_fn := message out_stream "G";
- Output.debug_fn := message out_stream "H";
- Output.prompt_fn := ignore;
- out_stream
- end;
-
-end;
-
-
-(* init *)
-
-fun init out =
- (change print_mode (update (op =) isabelle_processN);
- setup_channels out |> init_message;
- OuterKeyword.report ();
- Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
-
-end;
--- a/src/Pure/Tools/isabelle_process.scala Sat Feb 28 17:09:32 2009 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,435 +0,0 @@
-/* Title: Pure/Tools/isabelle_process.ML
- Author: Makarius
- Options: :folding=explicit:collapseFolds=1:
-
-Isabelle process management -- always reactive due to multi-threaded I/O.
-*/
-
-package isabelle
-
-import java.util.concurrent.LinkedBlockingQueue
-import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
- InputStream, OutputStream, IOException}
-
-
-object IsabelleProcess {
-
- /* results */
-
- object Kind extends Enumeration {
- //{{{ values and codes
- // internal system notification
- val SYSTEM = Value("SYSTEM")
- // Posix channels/events
- val STDIN = Value("STDIN")
- val STDOUT = Value("STDOUT")
- val SIGNAL = Value("SIGNAL")
- val EXIT = Value("EXIT")
- // Isabelle messages
- val INIT = Value("INIT")
- val STATUS = Value("STATUS")
- val WRITELN = Value("WRITELN")
- val PRIORITY = Value("PRIORITY")
- val TRACING = Value("TRACING")
- val WARNING = Value("WARNING")
- val ERROR = Value("ERROR")
- val DEBUG = Value("DEBUG")
- // messages codes
- val code = Map(
- ('A' : Int) -> Kind.INIT,
- ('B' : Int) -> Kind.STATUS,
- ('C' : Int) -> Kind.WRITELN,
- ('D' : Int) -> Kind.PRIORITY,
- ('E' : Int) -> Kind.TRACING,
- ('F' : Int) -> Kind.WARNING,
- ('G' : Int) -> Kind.ERROR,
- ('H' : Int) -> Kind.DEBUG,
- ('0' : Int) -> Kind.SYSTEM,
- ('1' : Int) -> Kind.STDIN,
- ('2' : Int) -> Kind.STDOUT,
- ('3' : Int) -> Kind.SIGNAL,
- ('4' : Int) -> Kind.EXIT)
- // message markup
- val markup = Map(
- Kind.INIT -> Markup.INIT,
- Kind.STATUS -> Markup.STATUS,
- Kind.WRITELN -> Markup.WRITELN,
- Kind.PRIORITY -> Markup.PRIORITY,
- Kind.TRACING -> Markup.TRACING,
- Kind.WARNING -> Markup.WARNING,
- Kind.ERROR -> Markup.ERROR,
- Kind.DEBUG -> Markup.DEBUG,
- Kind.SYSTEM -> Markup.SYSTEM,
- Kind.STDIN -> Markup.STDIN,
- Kind.STDOUT -> Markup.STDOUT,
- Kind.SIGNAL -> Markup.SIGNAL,
- Kind.EXIT -> Markup.EXIT)
- //}}}
- def is_raw(kind: Value) =
- kind == STDOUT
- def is_control(kind: Value) =
- kind == SYSTEM ||
- kind == SIGNAL ||
- kind == EXIT
- def is_system(kind: Value) =
- kind == SYSTEM ||
- kind == STDIN ||
- kind == SIGNAL ||
- kind == EXIT ||
- kind == STATUS
- }
-
- class Result(val kind: Kind.Value, val props: List[(String, String)], val result: String) {
- override def toString = {
- val trees = YXML.parse_body_failsafe(result)
- val res =
- if (kind == Kind.STATUS) trees.map(_.toString).mkString
- else trees.flatMap(XML.content(_).mkString).mkString
- if (props.isEmpty)
- kind.toString + " [[" + res + "]]"
- else
- kind.toString + " " +
- (for ((x, y) <- props) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
- }
- def is_raw = Kind.is_raw(kind)
- def is_control = Kind.is_control(kind)
- def is_system = Kind.is_system(kind)
- }
-
- def parse_message(isabelle_system: IsabelleSystem, result: Result) =
- {
- XML.Elem(Markup.MESSAGE, (Markup.CLASS, Kind.markup(result.kind)) :: result.props,
- YXML.parse_body_failsafe(isabelle_system.symbols.decode(result.result)))
- }
-}
-
-
-class IsabelleProcess(isabelle_system: IsabelleSystem,
- results: EventBus[IsabelleProcess.Result], args: String*)
-{
- import IsabelleProcess._
-
-
- /* demo constructor */
-
- def this(args: String*) =
- this(new IsabelleSystem, new EventBus[IsabelleProcess.Result] + Console.println, args: _*)
-
-
- /* process information */
-
- @volatile private var proc: Process = null
- @volatile private var closing = false
- @volatile private var pid: String = null
- @volatile private var the_session: String = null
- def session = the_session
-
-
- /* results */
-
- def parse_message(result: Result): XML.Tree =
- IsabelleProcess.parse_message(isabelle_system, result)
-
- private val result_queue = new LinkedBlockingQueue[Result]
-
- private def put_result(kind: Kind.Value, props: List[(String, String)], result: String)
- {
- if (kind == Kind.INIT) {
- val map = Map(props: _*)
- if (map.isDefinedAt(Markup.PID)) pid = map(Markup.PID)
- if (map.isDefinedAt(Markup.SESSION)) the_session = map(Markup.SESSION)
- }
- result_queue.put(new Result(kind, props, result))
- }
-
- private class ResultThread extends Thread("isabelle: results") {
- override def run() = {
- var finished = false
- while (!finished) {
- val result =
- try { result_queue.take }
- catch { case _: NullPointerException => null }
-
- if (result != null) {
- results.event(result)
- if (result.kind == Kind.EXIT) finished = true
- }
- else finished = true
- }
- }
- }
-
-
- /* signals */
-
- def interrupt() = synchronized {
- if (proc == null) error("Cannot interrupt Isabelle: no process")
- if (pid == null) put_result(Kind.SYSTEM, Nil, "Cannot interrupt: unknown pid")
- else {
- try {
- if (isabelle_system.execute(true, "kill", "-INT", pid).waitFor == 0)
- put_result(Kind.SIGNAL, Nil, "INT")
- else
- put_result(Kind.SYSTEM, Nil, "Cannot interrupt: kill command failed")
- }
- catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
- }
- }
-
- def kill() = synchronized {
- if (proc == 0) error("Cannot kill Isabelle: no process")
- else {
- try_close()
- Thread.sleep(500)
- put_result(Kind.SIGNAL, Nil, "KILL")
- proc.destroy
- proc = null
- pid = null
- }
- }
-
-
- /* output being piped into the process */
-
- private val output = new LinkedBlockingQueue[String]
-
- private def output_raw(text: String) = synchronized {
- if (proc == null) error("Cannot output to Isabelle: no process")
- if (closing) error("Cannot output to Isabelle: already closing")
- output.put(text)
- }
-
- def output_sync(text: String) =
- output_raw(" \\<^sync>\n; " + text + " \\<^sync>;\n")
-
-
- def command(text: String) =
- output_sync("Isabelle.command " + IsabelleSyntax.encode_string(text))
-
- def command(props: List[(String, String)], text: String) =
- output_sync("Isabelle.command " + IsabelleSyntax.encode_properties(props) + " " +
- IsabelleSyntax.encode_string(text))
-
- def ML(text: String) =
- output_sync("ML_val " + IsabelleSyntax.encode_string(text))
-
- def close() = synchronized { // FIXME watchdog/timeout
- output_raw("\u0000")
- closing = true
- }
-
- def try_close() = synchronized {
- if (proc != null && !closing) {
- try { close() }
- catch { case _: RuntimeException => }
- }
- }
-
-
- /* stdin */
-
- private class StdinThread(out_stream: OutputStream) extends Thread("isabelle: stdin") {
- override def run() = {
- val writer = new BufferedWriter(new OutputStreamWriter(out_stream, isabelle_system.charset))
- var finished = false
- while (!finished) {
- try {
- //{{{
- val s = output.take
- if (s == "\u0000") {
- writer.close
- finished = true
- }
- else {
- put_result(Kind.STDIN, Nil, s)
- writer.write(s)
- writer.flush
- }
- //}}}
- }
- catch {
- case e: IOException => put_result(Kind.SYSTEM, Nil, "Stdin thread: " + e.getMessage)
- }
- }
- put_result(Kind.SYSTEM, Nil, "Stdin thread terminated")
- }
- }
-
-
- /* stdout */
-
- private class StdoutThread(in_stream: InputStream) extends Thread("isabelle: stdout") {
- override def run() = {
- val reader = new BufferedReader(new InputStreamReader(in_stream, isabelle_system.charset))
- var result = new StringBuilder(100)
-
- var finished = false
- while (!finished) {
- try {
- //{{{
- var c = -1
- var done = false
- while (!done && (result.length == 0 || reader.ready)) {
- c = reader.read
- if (c >= 0) result.append(c.asInstanceOf[Char])
- else done = true
- }
- if (result.length > 0) {
- put_result(Kind.STDOUT, Nil, result.toString)
- result.length = 0
- }
- else {
- reader.close
- finished = true
- try_close()
- }
- //}}}
- }
- catch {
- case e: IOException => put_result(Kind.SYSTEM, Nil, "Stdout thread: " + e.getMessage)
- }
- }
- put_result(Kind.SYSTEM, Nil, "Stdout thread terminated")
- }
- }
-
-
- /* messages */
-
- private class MessageThread(fifo: String) extends Thread("isabelle: messages") {
- override def run() = {
- val reader = isabelle_system.fifo_reader(fifo)
- var kind: Kind.Value = null
- var props: List[(String, String)] = Nil
- var result = new StringBuilder
-
- var finished = false
- while (!finished) {
- try {
- if (kind == null) {
- //{{{ Char mode -- resync
- var c = -1
- do {
- c = reader.read
- if (c >= 0 && c != 2) result.append(c.asInstanceOf[Char])
- } while (c >= 0 && c != 2)
-
- if (result.length > 0) {
- put_result(Kind.SYSTEM, Nil, "Malformed message:\n" + result.toString)
- result.length = 0
- }
- if (c < 0) {
- reader.close
- finished = true
- try_close()
- }
- else {
- c = reader.read
- if (Kind.code.isDefinedAt(c)) kind = Kind.code(c)
- else kind = null
- }
- //}}}
- }
- else {
- //{{{ Line mode
- val line = reader.readLine
- if (line == null) {
- reader.close
- finished = true
- try_close()
- }
- else {
- val len = line.length
- // property
- if (line.endsWith("\u0002,")) {
- val i = line.indexOf('=')
- if (i > 0) {
- val name = line.substring(0, i)
- val value = line.substring(i + 1, len - 2)
- props = (name, value) :: props
- }
- }
- // last text line
- else if (line.endsWith("\u0002.")) {
- result.append(line.substring(0, len - 2))
- put_result(kind, props.reverse, result.toString)
- kind = null
- props = Nil
- result.length = 0
- }
- // text line
- else {
- result.append(line)
- result.append('\n')
- }
- }
- //}}}
- }
- }
- catch {
- case e: IOException => put_result(Kind.SYSTEM, Nil, "Message thread: " + e.getMessage)
- }
- }
- put_result(Kind.SYSTEM, Nil, "Message thread terminated")
- }
- }
-
-
-
- /** main **/
-
- {
- /* isabelle version */
-
- {
- val (msg, rc) = isabelle_system.isabelle_tool("version")
- if (rc != 0) error("Version check failed -- bad Isabelle installation:\n" + msg)
- put_result(Kind.SYSTEM, Nil, msg)
- }
-
-
- /* messages */
-
- val message_fifo = isabelle_system.mk_fifo()
- def rm_fifo() = isabelle_system.rm_fifo(message_fifo)
-
- val message_thread = new MessageThread(message_fifo)
- message_thread.start
-
- new ResultThread().start
-
-
- /* exec process */
-
- try {
- val cmdline =
- List(isabelle_system.getenv_strict("ISABELLE_PROCESS"), "-W", message_fifo) ++ args
- proc = isabelle_system.execute(true, cmdline: _*)
- }
- catch {
- case e: IOException =>
- rm_fifo()
- error("Failed to execute Isabelle process: " + e.getMessage)
- }
-
-
- /* stdin/stdout */
-
- new StdinThread(proc.getOutputStream).start
- new StdoutThread(proc.getInputStream).start
-
-
- /* exit */
-
- new Thread("isabelle: exit") {
- override def run() = {
- val rc = proc.waitFor()
- Thread.sleep(300)
- put_result(Kind.SYSTEM, Nil, "Exit thread terminated")
- put_result(Kind.EXIT, Nil, Integer.toString(rc))
- rm_fifo()
- }
- }.start
-
- }
-}