moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
1.1 --- a/src/Pure/IsaMakefile Sat Feb 28 17:09:32 2009 +0100
1.2 +++ b/src/Pure/IsaMakefile Sat Feb 28 18:00:20 2009 +0100
1.3 @@ -59,18 +59,17 @@
1.4 Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML \
1.5 Isar/class_target.ML Isar/code.ML Isar/code_unit.ML \
1.6 Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML \
1.7 - Isar/expression.ML Isar/isar.ML Isar/isar_cmd.ML \
1.8 - Isar/isar_document.ML Isar/isar_syn.ML Isar/local_defs.ML \
1.9 - Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML \
1.10 - Isar/method.ML Isar/net_rules.ML Isar/object_logic.ML Isar/obtain.ML \
1.11 - Isar/outer_keyword.ML Isar/outer_lex.ML Isar/outer_parse.ML \
1.12 - Isar/outer_syntax.ML Isar/overloading.ML Isar/proof.ML \
1.13 - Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML \
1.14 - Isar/rule_cases.ML Isar/rule_insts.ML Isar/session.ML \
1.15 - Isar/skip_proof.ML Isar/spec_parse.ML Isar/specification.ML \
1.16 - Isar/theory_target.ML Isar/toplevel.ML Isar/value_parse.ML \
1.17 - ML/ml_antiquote.ML ML/ml_context.ML ML/ml_lex.ML ML/ml_parse.ML \
1.18 - ML/ml_syntax.ML ML/ml_thms.ML Proof/extraction.ML \
1.19 + Isar/expression.ML Isar/isar_cmd.ML Isar/isar_document.ML \
1.20 + Isar/isar_syn.ML Isar/local_defs.ML Isar/local_syntax.ML \
1.21 + Isar/local_theory.ML Isar/locale.ML Isar/method.ML Isar/net_rules.ML \
1.22 + Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML \
1.23 + Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML \
1.24 + Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML \
1.25 + Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML \
1.26 + Isar/rule_insts.ML Isar/skip_proof.ML Isar/spec_parse.ML \
1.27 + Isar/specification.ML Isar/theory_target.ML Isar/toplevel.ML \
1.28 + Isar/value_parse.ML ML/ml_antiquote.ML ML/ml_context.ML ML/ml_lex.ML \
1.29 + ML/ml_parse.ML ML/ml_syntax.ML ML/ml_thms.ML Proof/extraction.ML \
1.30 Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML \
1.31 Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/ROOT.ML \
1.32 ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML \
1.33 @@ -81,11 +80,12 @@
1.34 ProofGeneral/proof_general_pgip.ML Pure.thy ROOT.ML Syntax/ast.ML \
1.35 Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML \
1.36 Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML \
1.37 - Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML \
1.38 - Thy/latex.ML Thy/present.ML Thy/term_style.ML Thy/thm_deps.ML \
1.39 - Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML Thy/thy_output.ML \
1.40 - Thy/thy_syntax.ML Tools/ROOT.ML Tools/find_consts.ML \
1.41 - Tools/find_theorems.ML Tools/isabelle_process.ML Tools/named_thms.ML \
1.42 + Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML \
1.43 + System/isabelle_process.ML System/isar.ML System/session.ML \
1.44 + Thy/html.ML Thy/latex.ML Thy/present.ML Thy/term_style.ML \
1.45 + Thy/thm_deps.ML Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML \
1.46 + Thy/thy_output.ML Thy/thy_syntax.ML Tools/ROOT.ML \
1.47 + Tools/find_consts.ML Tools/find_theorems.ML Tools/named_thms.ML \
1.48 Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML config.ML \
1.49 conjunction.ML consts.ML context.ML context_position.ML conv.ML \
1.50 defs.ML display.ML drule.ML envir.ML facts.ML goal.ML \
1.51 @@ -119,7 +119,7 @@
1.52 General/position.scala General/swing.scala General/symbol.scala \
1.53 General/xml.scala General/yxml.scala Isar/isar.scala \
1.54 Isar/isar_document.scala Isar/outer_keyword.scala \
1.55 - Thy/thy_header.scala Tools/isabelle_process.scala \
1.56 + System/isabelle_process.scala Thy/thy_header.scala \
1.57 Tools/isabelle_syntax.scala Tools/isabelle_system.scala
1.58
1.59
2.1 --- a/src/Pure/Isar/ROOT.ML Sat Feb 28 17:09:32 2009 +0100
2.2 +++ b/src/Pure/Isar/ROOT.ML Sat Feb 28 18:00:20 2009 +0100
2.3 @@ -82,8 +82,6 @@
2.4 use "../old_goals.ML";
2.5 use "outer_syntax.ML";
2.6 use "../Thy/thy_info.ML";
2.7 -use "session.ML";
2.8 -use "isar.ML";
2.9 use "isar_document.ML";
2.10
2.11 (*theory and proof operations*)
2.12 @@ -91,3 +89,5 @@
2.13 use "../Thy/thm_deps.ML";
2.14 use "isar_cmd.ML";
2.15 use "isar_syn.ML";
2.16 +
2.17 +
3.1 --- a/src/Pure/Isar/isar.ML Sat Feb 28 17:09:32 2009 +0100
3.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
3.3 @@ -1,379 +0,0 @@
3.4 -(* Title: Pure/Isar/isar.ML
3.5 - Author: Makarius
3.6 -
3.7 -The global Isabelle/Isar state and main read-eval-print loop.
3.8 -*)
3.9 -
3.10 -signature ISAR =
3.11 -sig
3.12 - val init: unit -> unit
3.13 - val exn: unit -> (exn * string) option
3.14 - val state: unit -> Toplevel.state
3.15 - val context: unit -> Proof.context
3.16 - val goal: unit -> thm
3.17 - val print: unit -> unit
3.18 - val >> : Toplevel.transition -> bool
3.19 - val >>> : Toplevel.transition list -> unit
3.20 - val linear_undo: int -> unit
3.21 - val undo: int -> unit
3.22 - val kill: unit -> unit
3.23 - val kill_proof: unit -> unit
3.24 - val crashes: exn list ref
3.25 - val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
3.26 - val loop: unit -> unit
3.27 - val main: unit -> unit
3.28 -
3.29 - type id = string
3.30 - val no_id: id
3.31 - val create_command: Toplevel.transition -> id
3.32 - val insert_command: id -> id -> unit
3.33 - val remove_command: id -> unit
3.34 -end;
3.35 -
3.36 -structure Isar: ISAR =
3.37 -struct
3.38 -
3.39 -
3.40 -(** TTY model -- SINGLE-THREADED! **)
3.41 -
3.42 -(* the global state *)
3.43 -
3.44 -type history = (Toplevel.state * Toplevel.transition) list;
3.45 - (*previous state, state transition -- regular commands only*)
3.46 -
3.47 -local
3.48 - val global_history = ref ([]: history);
3.49 - val global_state = ref Toplevel.toplevel;
3.50 - val global_exn = ref (NONE: (exn * string) option);
3.51 -in
3.52 -
3.53 -fun edit_history count f = NAMED_CRITICAL "Isar" (fn () =>
3.54 - let
3.55 - fun edit 0 (st, hist) = (global_history := hist; global_state := st; global_exn := NONE)
3.56 - | edit n (st, hist) = edit (n - 1) (f st hist);
3.57 - in edit count (! global_state, ! global_history) end);
3.58 -
3.59 -fun state () = NAMED_CRITICAL "Isar" (fn () => ! global_state);
3.60 -fun set_state state = NAMED_CRITICAL "Isar" (fn () => global_state := state);
3.61 -
3.62 -fun exn () = NAMED_CRITICAL "Isar" (fn () => ! global_exn);
3.63 -fun set_exn exn = NAMED_CRITICAL "Isar" (fn () => global_exn := exn);
3.64 -
3.65 -end;
3.66 -
3.67 -
3.68 -fun init () = edit_history 1 (K (K (Toplevel.toplevel, [])));
3.69 -
3.70 -fun context () = Toplevel.context_of (state ())
3.71 - handle Toplevel.UNDEF => error "Unknown context";
3.72 -
3.73 -fun goal () = #2 (#2 (Proof.get_goal (Toplevel.proof_of (state ()))))
3.74 - handle Toplevel.UNDEF => error "No goal present";
3.75 -
3.76 -fun print () = Toplevel.print_state false (state ());
3.77 -
3.78 -
3.79 -(* history navigation *)
3.80 -
3.81 -local
3.82 -
3.83 -fun find_and_undo _ [] = error "Undo history exhausted"
3.84 - | find_and_undo which ((prev, tr) :: hist) =
3.85 - ((case Toplevel.init_of tr of SOME name => ThyInfo.kill_thy name | NONE => ());
3.86 - if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist);
3.87 -
3.88 -in
3.89 -
3.90 -fun linear_undo n = edit_history n (K (find_and_undo (K true)));
3.91 -
3.92 -fun undo n = edit_history n (fn st => fn hist =>
3.93 - find_and_undo (if Toplevel.is_proof st then K true else OuterKeyword.is_theory) hist);
3.94 -
3.95 -fun kill () = edit_history 1 (fn st => fn hist =>
3.96 - find_and_undo
3.97 - (if Toplevel.is_proof st then OuterKeyword.is_theory else OuterKeyword.is_theory_begin) hist);
3.98 -
3.99 -fun kill_proof () = edit_history 1 (fn st => fn hist =>
3.100 - if Toplevel.is_proof st then find_and_undo OuterKeyword.is_theory hist
3.101 - else raise Toplevel.UNDEF);
3.102 -
3.103 -end;
3.104 -
3.105 -
3.106 -(* interactive state transformations *)
3.107 -
3.108 -fun op >> tr =
3.109 - (case Toplevel.transition true tr (state ()) of
3.110 - NONE => false
3.111 - | SOME (_, SOME err) => (set_exn (SOME err); Toplevel.error_msg tr err; true)
3.112 - | SOME (st', NONE) =>
3.113 - let
3.114 - val name = Toplevel.name_of tr;
3.115 - val _ = if OuterKeyword.is_theory_begin name then init () else ();
3.116 - val _ =
3.117 - if OuterKeyword.is_regular name
3.118 - then edit_history 1 (fn st => fn hist => (st', (st, tr) :: hist)) else ();
3.119 - in true end);
3.120 -
3.121 -fun op >>> [] = ()
3.122 - | op >>> (tr :: trs) = if op >> tr then op >>> trs else ();
3.123 -
3.124 -
3.125 -(* toplevel loop *)
3.126 -
3.127 -val crashes = ref ([]: exn list);
3.128 -
3.129 -local
3.130 -
3.131 -fun raw_loop secure src =
3.132 - let
3.133 - fun check_secure () =
3.134 - (if secure then warning "Secure loop -- cannot exit to ML" else (); secure);
3.135 - in
3.136 - (case Source.get_single (Source.set_prompt Source.default_prompt src) of
3.137 - NONE => if secure then quit () else ()
3.138 - | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
3.139 - handle exn =>
3.140 - (Output.error_msg (Toplevel.exn_message exn)
3.141 - handle crash =>
3.142 - (CRITICAL (fn () => change crashes (cons crash));
3.143 - warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
3.144 - raw_loop secure src)
3.145 - end;
3.146 -
3.147 -in
3.148 -
3.149 -fun toplevel_loop {init = do_init, welcome, sync, secure} =
3.150 - (Context.set_thread_data NONE;
3.151 - if do_init then init () else (); (* FIXME init editor model *)
3.152 - if welcome then writeln (Session.welcome ()) else ();
3.153 - uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ());
3.154 -
3.155 -end;
3.156 -
3.157 -fun loop () =
3.158 - toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
3.159 -
3.160 -fun main () =
3.161 - toplevel_loop {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};
3.162 -
3.163 -
3.164 -
3.165 -(** individual toplevel commands **)
3.166 -
3.167 -(* unique identification *)
3.168 -
3.169 -type id = string;
3.170 -val no_id : id = "";
3.171 -
3.172 -
3.173 -(* command category *)
3.174 -
3.175 -datatype category = Empty | Theory | Proof | Diag | Control;
3.176 -
3.177 -fun category_of tr =
3.178 - let val name = Toplevel.name_of tr in
3.179 - if name = "" then Empty
3.180 - else if OuterKeyword.is_theory name then Theory
3.181 - else if OuterKeyword.is_proof name then Proof
3.182 - else if OuterKeyword.is_diag name then Diag
3.183 - else Control
3.184 - end;
3.185 -
3.186 -val is_theory = fn Theory => true | _ => false;
3.187 -val is_proper = fn Theory => true | Proof => true | _ => false;
3.188 -val is_regular = fn Control => false | _ => true;
3.189 -
3.190 -
3.191 -(* command status *)
3.192 -
3.193 -datatype status =
3.194 - Unprocessed |
3.195 - Running |
3.196 - Failed of exn * string |
3.197 - Finished of Toplevel.state;
3.198 -
3.199 -fun status_markup Unprocessed = Markup.unprocessed
3.200 - | status_markup Running = (Markup.runningN, [])
3.201 - | status_markup (Failed _) = Markup.failed
3.202 - | status_markup (Finished _) = Markup.finished;
3.203 -
3.204 -fun run int tr state =
3.205 - (case Toplevel.transition int tr state of
3.206 - NONE => NONE
3.207 - | SOME (_, SOME err) => (Toplevel.error_msg tr err; SOME (Failed err))
3.208 - | SOME (state', NONE) => SOME (Finished state'));
3.209 -
3.210 -
3.211 -(* datatype command *)
3.212 -
3.213 -datatype command = Command of
3.214 - {category: category,
3.215 - transition: Toplevel.transition,
3.216 - status: status};
3.217 -
3.218 -fun make_command (category, transition, status) =
3.219 - Command {category = category, transition = transition, status = status};
3.220 -
3.221 -val empty_command =
3.222 - make_command (Empty, Toplevel.empty, Finished Toplevel.toplevel);
3.223 -
3.224 -fun map_command f (Command {category, transition, status}) =
3.225 - make_command (f (category, transition, status));
3.226 -
3.227 -fun map_status f = map_command (fn (category, transition, status) =>
3.228 - (category, transition, f status));
3.229 -
3.230 -
3.231 -(* global collection of identified commands *)
3.232 -
3.233 -fun err_dup id = sys_error ("Duplicate command " ^ quote id);
3.234 -fun err_undef id = sys_error ("Unknown command " ^ quote id);
3.235 -
3.236 -local val global_commands = ref (Graph.empty: command Graph.T) in
3.237 -
3.238 -fun change_commands f = NAMED_CRITICAL "Isar" (fn () => change global_commands f)
3.239 - handle Graph.DUP bad => err_dup bad | Graph.UNDEF bad => err_undef bad;
3.240 -
3.241 -fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands);
3.242 -
3.243 -end;
3.244 -
3.245 -fun add_edge (id1, id2) =
3.246 - if id1 = no_id orelse id2 = no_id then I else Graph.add_edge (id1, id2);
3.247 -
3.248 -
3.249 -fun init_commands () = change_commands (K Graph.empty);
3.250 -
3.251 -fun the_command id =
3.252 - let val Command cmd =
3.253 - if id = no_id then empty_command
3.254 - else (Graph.get_node (get_commands ()) id handle Graph.UNDEF bad => err_undef bad)
3.255 - in cmd end;
3.256 -
3.257 -fun prev_command id =
3.258 - if id = no_id then no_id
3.259 - else
3.260 - (case Graph.imm_preds (get_commands ()) id handle Graph.UNDEF bad => err_undef bad of
3.261 - [] => no_id
3.262 - | [prev] => prev
3.263 - | _ => sys_error ("Non-linear command dependency " ^ quote id));
3.264 -
3.265 -fun next_commands id =
3.266 - if id = no_id then []
3.267 - else Graph.imm_succs (get_commands ()) id handle Graph.UNDEF bad => err_undef bad;
3.268 -
3.269 -fun descendant_commands ids =
3.270 - Graph.all_succs (get_commands ()) (distinct (op =) (filter_out (fn id => id = no_id) ids))
3.271 - handle Graph.UNDEF bad => err_undef bad;
3.272 -
3.273 -
3.274 -(* maintain status *)
3.275 -
3.276 -fun report_status markup id = Toplevel.status (#transition (the_command id)) markup;
3.277 -
3.278 -fun update_status status id = change_commands (Graph.map_node id (map_status (K status)));
3.279 -
3.280 -fun report_update_status status id =
3.281 - change_commands (Graph.map_node id (map_status (fn old_status =>
3.282 - let val markup = status_markup status
3.283 - in if markup <> status_markup old_status then report_status markup id else (); status end)));
3.284 -
3.285 -
3.286 -(* create and dispose commands *)
3.287 -
3.288 -fun create_command raw_tr =
3.289 - let
3.290 - val (id, tr) =
3.291 - (case Toplevel.get_id raw_tr of
3.292 - SOME id => (id, raw_tr)
3.293 - | NONE =>
3.294 - let val id =
3.295 - if ! Toplevel.debug then "isabelle:" ^ Toplevel.name_of raw_tr ^ serial_string ()
3.296 - else "isabelle:" ^ serial_string ()
3.297 - in (id, Toplevel.put_id id raw_tr) end);
3.298 -
3.299 - val cmd = make_command (category_of tr, tr, Unprocessed);
3.300 - val _ = change_commands (Graph.new_node (id, cmd));
3.301 - in id end;
3.302 -
3.303 -fun dispose_commands ids =
3.304 - let
3.305 - val desc = descendant_commands ids;
3.306 - val _ = List.app (report_status Markup.disposed) desc;
3.307 - val _ = change_commands (Graph.del_nodes desc);
3.308 - in () end;
3.309 -
3.310 -
3.311 -(* final state *)
3.312 -
3.313 -fun the_state id =
3.314 - (case the_command id of
3.315 - {status = Finished state, ...} => state
3.316 - | {transition, ...} => error ("Unfinished command " ^ Toplevel.str_of transition));
3.317 -
3.318 -
3.319 -
3.320 -(** editor model **)
3.321 -
3.322 -(* run commands *)
3.323 -
3.324 -fun try_run id =
3.325 - (case try the_state (prev_command id) of
3.326 - NONE => ()
3.327 - | SOME state =>
3.328 - (case run true (#transition (the_command id)) state of
3.329 - NONE => ()
3.330 - | SOME status => report_update_status status id));
3.331 -
3.332 -fun rerun_commands ids =
3.333 - (List.app (report_update_status Unprocessed) ids; List.app try_run ids);
3.334 -
3.335 -
3.336 -(* modify document *)
3.337 -
3.338 -fun insert_command prev id = NAMED_CRITICAL "Isar" (fn () =>
3.339 - let
3.340 - val nexts = next_commands prev;
3.341 - val _ = change_commands
3.342 - (fold (fn next => Graph.del_edge (prev, next)) nexts #> add_edge (prev, id) #>
3.343 - fold (fn next => Graph.add_edge (id, next)) nexts);
3.344 - in descendant_commands [id] end) |> rerun_commands;
3.345 -
3.346 -fun remove_command id = NAMED_CRITICAL "Isar" (fn () =>
3.347 - let
3.348 - val prev = prev_command id;
3.349 - val nexts = next_commands id;
3.350 - val _ = change_commands
3.351 - (fold (fn next => Graph.del_edge (id, next)) nexts #>
3.352 - fold (fn next => add_edge (prev, next)) nexts);
3.353 - in descendant_commands nexts end) |> rerun_commands;
3.354 -
3.355 -
3.356 -(* concrete syntax *)
3.357 -
3.358 -local
3.359 -
3.360 -structure P = OuterParse;
3.361 -val op >> = Scan.>>;
3.362 -
3.363 -in
3.364 -
3.365 -val _ =
3.366 - OuterSyntax.internal_command "Isar.command"
3.367 - (P.string -- P.string >> (fn (id, text) =>
3.368 - Toplevel.imperative (fn () =>
3.369 - ignore (create_command (OuterSyntax.prepare_command (Position.id id) text)))));
3.370 -
3.371 -val _ =
3.372 - OuterSyntax.internal_command "Isar.insert"
3.373 - (P.string -- P.string >> (fn (prev, id) =>
3.374 - Toplevel.imperative (fn () => insert_command prev id)));
3.375 -
3.376 -val _ =
3.377 - OuterSyntax.internal_command "Isar.remove"
3.378 - (P.string >> (fn id => Toplevel.imperative (fn () => remove_command id)));
3.379 -
3.380 -end;
3.381 -
3.382 -end;
4.1 --- a/src/Pure/Isar/isar_cmd.ML Sat Feb 28 17:09:32 2009 +0100
4.2 +++ b/src/Pure/Isar/isar_cmd.ML Sat Feb 28 18:00:20 2009 +0100
4.3 @@ -32,7 +32,6 @@
4.4 val skip_proof: Toplevel.transition -> Toplevel.transition
4.5 val init_theory: string * string list * (string * bool) list ->
4.6 Toplevel.transition -> Toplevel.transition
4.7 - val welcome: Toplevel.transition -> Toplevel.transition
4.8 val exit: Toplevel.transition -> Toplevel.transition
4.9 val quit: Toplevel.transition -> Toplevel.transition
4.10 val pr: string list * (int option * int option) -> Toplevel.transition -> Toplevel.transition
4.11 @@ -265,8 +264,6 @@
4.12 if ThyInfo.check_known_thy (Context.theory_name thy)
4.13 then ThyInfo.end_theory thy else ());
4.14
4.15 -val welcome = Toplevel.imperative (writeln o Session.welcome);
4.16 -
4.17 val exit = Toplevel.keep (fn state =>
4.18 (Context.set_thread_data (try Toplevel.generic_theory_of state);
4.19 raise Toplevel.TERMINATE));
5.1 --- a/src/Pure/Isar/isar_syn.ML Sat Feb 28 17:09:32 2009 +0100
5.2 +++ b/src/Pure/Isar/isar_syn.ML Sat Feb 28 18:00:20 2009 +0100
5.3 @@ -729,39 +729,6 @@
5.4 handle ERROR msg => Scan.fail_with (K msg)));
5.5
5.6
5.7 -(* global history commands *)
5.8 -
5.9 -val _ =
5.10 - OuterSyntax.improper_command "init_toplevel" "init toplevel point-of-interest" K.control
5.11 - (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.init));
5.12 -
5.13 -val _ =
5.14 - OuterSyntax.improper_command "linear_undo" "undo commands" K.control
5.15 - (Scan.optional P.nat 1 >>
5.16 - (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.linear_undo n)));
5.17 -
5.18 -val _ =
5.19 - OuterSyntax.improper_command "undo" "undo commands (skipping closed proofs)" K.control
5.20 - (Scan.optional P.nat 1 >>
5.21 - (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo n)));
5.22 -
5.23 -val _ =
5.24 - OuterSyntax.improper_command "undos_proof" "undo commands (skipping closed proofs)" K.control
5.25 - (Scan.optional P.nat 1 >> (fn n => Toplevel.no_timing o
5.26 - Toplevel.keep (fn state =>
5.27 - if Toplevel.is_proof state then (Isar.undo n; Isar.print ()) else raise Toplevel.UNDEF)));
5.28 -
5.29 -val _ =
5.30 - OuterSyntax.improper_command "cannot_undo" "partial undo -- Proof General legacy" K.control
5.31 - (P.name >>
5.32 - (fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)
5.33 - | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
5.34 -
5.35 -val _ =
5.36 - OuterSyntax.improper_command "kill" "kill partial proof or theory development" K.control
5.37 - (Scan.succeed (Toplevel.no_timing o Toplevel.imperative Isar.kill));
5.38 -
5.39 -
5.40
5.41 (** diagnostic commands (for interactive mode only) **)
5.42
5.43 @@ -974,9 +941,5 @@
5.44 OuterSyntax.improper_command "exit" "exit Isar loop" K.control
5.45 (Scan.succeed (Toplevel.no_timing o IsarCmd.exit));
5.46
5.47 -val _ =
5.48 - OuterSyntax.improper_command "welcome" "print welcome message" K.diag
5.49 - (Scan.succeed (Toplevel.no_timing o IsarCmd.welcome));
5.50 -
5.51 end;
5.52
6.1 --- a/src/Pure/Isar/session.ML Sat Feb 28 17:09:32 2009 +0100
6.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
6.3 @@ -1,105 +0,0 @@
6.4 -(* Title: Pure/Isar/session.ML
6.5 - Author: Markus Wenzel, TU Muenchen
6.6 -
6.7 -Session management -- maintain state of logic images.
6.8 -*)
6.9 -
6.10 -signature SESSION =
6.11 -sig
6.12 - val id: unit -> string list
6.13 - val name: unit -> string
6.14 - val welcome: unit -> string
6.15 - val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool -> string list ->
6.16 - string -> string -> bool * string -> string -> int -> bool -> int -> int -> bool -> unit
6.17 - val finish: unit -> unit
6.18 -end;
6.19 -
6.20 -structure Session: SESSION =
6.21 -struct
6.22 -
6.23 -
6.24 -(* session state *)
6.25 -
6.26 -val session = ref ([Context.PureN]: string list);
6.27 -val session_path = ref ([]: string list);
6.28 -val session_finished = ref false;
6.29 -val remote_path = ref (NONE: Url.T option);
6.30 -
6.31 -
6.32 -(* access path *)
6.33 -
6.34 -fun id () = ! session;
6.35 -fun path () = ! session_path;
6.36 -
6.37 -fun str_of [] = Context.PureN
6.38 - | str_of elems = space_implode "/" elems;
6.39 -
6.40 -fun name () = "Isabelle/" ^ str_of (path ());
6.41 -
6.42 -fun welcome () =
6.43 - if Distribution.is_official then
6.44 - "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
6.45 - else
6.46 - "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")" ^
6.47 - (if Distribution.changelog <> "" then "\nSee also " ^ Distribution.changelog else "");
6.48 -
6.49 -
6.50 -(* add_path *)
6.51 -
6.52 -fun add_path reset s =
6.53 - let val sess = ! session @ [s] in
6.54 - (case duplicates (op =) sess of
6.55 - [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
6.56 - | dups => error ("Duplicate session identifiers " ^ commas_quote dups ^ " in " ^ str_of sess))
6.57 - end;
6.58 -
6.59 -
6.60 -(* init *)
6.61 -
6.62 -fun init reset parent name =
6.63 - if not (member (op =) (! session) parent) orelse not (! session_finished) then
6.64 - error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
6.65 - else (add_path reset name; session_finished := false);
6.66 -
6.67 -
6.68 -(* finish *)
6.69 -
6.70 -fun finish () =
6.71 - (Output.accumulated_time ();
6.72 - ThyInfo.finish ();
6.73 - Present.finish ();
6.74 - Future.shutdown ();
6.75 - session_finished := true);
6.76 -
6.77 -
6.78 -(* use_dir *)
6.79 -
6.80 -fun get_rpath rpath =
6.81 - (if rpath = "" then () else
6.82 - if is_some (! remote_path) then
6.83 - error "Path for remote theory browsing information may only be set once"
6.84 - else
6.85 - remote_path := SOME (Url.explode rpath);
6.86 - (! remote_path, rpath <> ""));
6.87 -
6.88 -fun dumping (_, "") = NONE
6.89 - | dumping (cp, path) = SOME (cp, Path.explode path);
6.90 -
6.91 -fun use_dir root build modes reset info doc doc_graph doc_versions
6.92 - parent name dump rpath level verbose max_threads trace_threads parallel_proofs =
6.93 - ((fn () =>
6.94 - (init reset parent name;
6.95 - Present.init build info doc doc_graph doc_versions (path ()) name
6.96 - (dumping dump) (get_rpath rpath) verbose (map ThyInfo.get_theory (ThyInfo.get_names ()));
6.97 - use root;
6.98 - finish ()))
6.99 - |> setmp_noncritical Proofterm.proofs level
6.100 - |> setmp_noncritical print_mode (modes @ print_mode_value ())
6.101 - |> setmp_noncritical Goal.parallel_proofs parallel_proofs
6.102 - |> setmp_noncritical Multithreading.trace trace_threads
6.103 - |> setmp_noncritical Multithreading.max_threads
6.104 - (if Multithreading.available then max_threads
6.105 - else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
6.106 - handle exn => (Output.error_msg (Toplevel.exn_message exn); exit 1);
6.107 -
6.108 -end;
7.1 --- a/src/Pure/ROOT.ML Sat Feb 28 17:09:32 2009 +0100
7.2 +++ b/src/Pure/ROOT.ML Sat Feb 28 18:00:20 2009 +0100
7.3 @@ -81,12 +81,18 @@
7.4 use "goal.ML";
7.5 use "axclass.ML";
7.6
7.7 -(*the main Isar system*)
7.8 +(*main Isar stuff*)
7.9 cd "Isar"; use "ROOT.ML"; cd "..";
7.10 use "subgoal.ML";
7.11
7.12 use "Proof/extraction.ML";
7.13
7.14 +(*Isabelle/Isar system*)
7.15 +use "System/session.ML";
7.16 +use "System/isar.ML";
7.17 +use "System/isabelle_process.ML";
7.18 +
7.19 +(*additional tools*)
7.20 cd "Tools"; use "ROOT.ML"; cd "..";
7.21
7.22 use "codegen.ML";
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/Pure/System/isabelle_process.ML Sat Feb 28 18:00:20 2009 +0100
8.3 @@ -0,0 +1,138 @@
8.4 +(* Title: Pure/System/isabelle_process.ML
8.5 + Author: Makarius
8.6 +
8.7 +Isabelle process wrapper -- interaction via external program.
8.8 +
8.9 +General format of process output:
8.10 +
8.11 + (1) unmarked stdout/stderr, no line structure (output should be
8.12 + processed immediately as it arrives);
8.13 +
8.14 + (2) properly marked-up messages, e.g. for writeln channel
8.15 +
8.16 + "\002A" ^ props ^ "\002,\n" ^ text ^ "\002.\n"
8.17 +
8.18 + where the props consist of name=value lines terminated by "\002,\n"
8.19 + each, and the remaining text is any number of lines (output is
8.20 + supposed to be processed in one piece);
8.21 +
8.22 + (3) special init message holds "pid" and "session" property;
8.23 +
8.24 + (4) message content is encoded in YXML format.
8.25 +*)
8.26 +
8.27 +signature ISABELLE_PROCESS =
8.28 +sig
8.29 + val isabelle_processN: string
8.30 + val init: string -> unit
8.31 +end;
8.32 +
8.33 +structure IsabelleProcess: ISABELLE_PROCESS =
8.34 +struct
8.35 +
8.36 +(* print modes *)
8.37 +
8.38 +val isabelle_processN = "isabelle_process";
8.39 +
8.40 +val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
8.41 +val _ = Markup.add_mode isabelle_processN YXML.output_markup;
8.42 +
8.43 +
8.44 +(* message markup *)
8.45 +
8.46 +fun special ch = Symbol.STX ^ ch;
8.47 +val special_sep = special ",";
8.48 +val special_end = special ".";
8.49 +
8.50 +local
8.51 +
8.52 +fun clean_string bad str =
8.53 + if exists_string (member (op =) bad) str then
8.54 + translate_string (fn c => if member (op =) bad c then Symbol.DEL else c) str
8.55 + else str;
8.56 +
8.57 +fun message_props props =
8.58 + let val clean = clean_string [Symbol.STX, "\n", "\r"]
8.59 + in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end;
8.60 +
8.61 +fun message_pos trees = trees |> get_first
8.62 + (fn XML.Elem (name, atts, ts) =>
8.63 + if name = Markup.positionN then SOME (Position.of_properties atts)
8.64 + else message_pos ts
8.65 + | _ => NONE);
8.66 +
8.67 +fun output out_stream s = NAMED_CRITICAL "IO" (fn () =>
8.68 + (TextIO.output (out_stream, s); TextIO.output (out_stream, "\n")));
8.69 +
8.70 +in
8.71 +
8.72 +fun message _ _ "" = ()
8.73 + | message out_stream ch body =
8.74 + let
8.75 + val pos = the_default Position.none (message_pos (YXML.parse_body body));
8.76 + val props =
8.77 + Position.properties_of (Position.thread_data ())
8.78 + |> Position.default_properties pos;
8.79 + val txt = clean_string [Symbol.STX] body;
8.80 + in output out_stream (special ch ^ message_props props ^ txt ^ special_end) end;
8.81 +
8.82 +fun init_message out_stream =
8.83 + let
8.84 + val pid = (Markup.pidN, process_id ());
8.85 + val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown");
8.86 + val text = Session.welcome ();
8.87 + in output out_stream (special "A" ^ message_props [pid, session] ^ text ^ special_end) end;
8.88 +
8.89 +end;
8.90 +
8.91 +
8.92 +(* channels *)
8.93 +
8.94 +local
8.95 +
8.96 +fun auto_flush stream =
8.97 + let
8.98 + val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream stream, IO.BLOCK_BUF);
8.99 + fun loop () =
8.100 + (OS.Process.sleep (Time.fromMilliseconds 50); try TextIO.flushOut stream; loop ());
8.101 + in loop end;
8.102 +
8.103 +in
8.104 +
8.105 +fun setup_channels out =
8.106 + let
8.107 + val out_stream =
8.108 + if out = "-" then TextIO.stdOut
8.109 + else
8.110 + let
8.111 + val path = File.platform_path (Path.explode out);
8.112 + val out_stream = TextIO.openOut path; (*fifo blocks until reader is ready*)
8.113 + val _ = OS.FileSys.remove path; (*prevent alien access, indicate writer is ready*)
8.114 + val _ = SimpleThread.fork false (auto_flush TextIO.stdOut);
8.115 + in out_stream end;
8.116 + val _ = SimpleThread.fork false (auto_flush out_stream);
8.117 + val _ = SimpleThread.fork false (auto_flush TextIO.stdErr);
8.118 + in
8.119 + Output.status_fn := message out_stream "B";
8.120 + Output.writeln_fn := message out_stream "C";
8.121 + Output.priority_fn := message out_stream "D";
8.122 + Output.tracing_fn := message out_stream "E";
8.123 + Output.warning_fn := message out_stream "F";
8.124 + Output.error_fn := message out_stream "G";
8.125 + Output.debug_fn := message out_stream "H";
8.126 + Output.prompt_fn := ignore;
8.127 + out_stream
8.128 + end;
8.129 +
8.130 +end;
8.131 +
8.132 +
8.133 +(* init *)
8.134 +
8.135 +fun init out =
8.136 + (change print_mode (update (op =) isabelle_processN);
8.137 + setup_channels out |> init_message;
8.138 + OuterKeyword.report ();
8.139 + Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
8.140 +
8.141 +end;
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/Pure/System/isabelle_process.scala Sat Feb 28 18:00:20 2009 +0100
9.3 @@ -0,0 +1,435 @@
9.4 +/* Title: Pure/System/isabelle_process.ML
9.5 + Author: Makarius
9.6 + Options: :folding=explicit:collapseFolds=1:
9.7 +
9.8 +Isabelle process management -- always reactive due to multi-threaded I/O.
9.9 +*/
9.10 +
9.11 +package isabelle
9.12 +
9.13 +import java.util.concurrent.LinkedBlockingQueue
9.14 +import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
9.15 + InputStream, OutputStream, IOException}
9.16 +
9.17 +
9.18 +object IsabelleProcess {
9.19 +
9.20 + /* results */
9.21 +
9.22 + object Kind extends Enumeration {
9.23 + //{{{ values and codes
9.24 + // internal system notification
9.25 + val SYSTEM = Value("SYSTEM")
9.26 + // Posix channels/events
9.27 + val STDIN = Value("STDIN")
9.28 + val STDOUT = Value("STDOUT")
9.29 + val SIGNAL = Value("SIGNAL")
9.30 + val EXIT = Value("EXIT")
9.31 + // Isabelle messages
9.32 + val INIT = Value("INIT")
9.33 + val STATUS = Value("STATUS")
9.34 + val WRITELN = Value("WRITELN")
9.35 + val PRIORITY = Value("PRIORITY")
9.36 + val TRACING = Value("TRACING")
9.37 + val WARNING = Value("WARNING")
9.38 + val ERROR = Value("ERROR")
9.39 + val DEBUG = Value("DEBUG")
9.40 + // messages codes
9.41 + val code = Map(
9.42 + ('A' : Int) -> Kind.INIT,
9.43 + ('B' : Int) -> Kind.STATUS,
9.44 + ('C' : Int) -> Kind.WRITELN,
9.45 + ('D' : Int) -> Kind.PRIORITY,
9.46 + ('E' : Int) -> Kind.TRACING,
9.47 + ('F' : Int) -> Kind.WARNING,
9.48 + ('G' : Int) -> Kind.ERROR,
9.49 + ('H' : Int) -> Kind.DEBUG,
9.50 + ('0' : Int) -> Kind.SYSTEM,
9.51 + ('1' : Int) -> Kind.STDIN,
9.52 + ('2' : Int) -> Kind.STDOUT,
9.53 + ('3' : Int) -> Kind.SIGNAL,
9.54 + ('4' : Int) -> Kind.EXIT)
9.55 + // message markup
9.56 + val markup = Map(
9.57 + Kind.INIT -> Markup.INIT,
9.58 + Kind.STATUS -> Markup.STATUS,
9.59 + Kind.WRITELN -> Markup.WRITELN,
9.60 + Kind.PRIORITY -> Markup.PRIORITY,
9.61 + Kind.TRACING -> Markup.TRACING,
9.62 + Kind.WARNING -> Markup.WARNING,
9.63 + Kind.ERROR -> Markup.ERROR,
9.64 + Kind.DEBUG -> Markup.DEBUG,
9.65 + Kind.SYSTEM -> Markup.SYSTEM,
9.66 + Kind.STDIN -> Markup.STDIN,
9.67 + Kind.STDOUT -> Markup.STDOUT,
9.68 + Kind.SIGNAL -> Markup.SIGNAL,
9.69 + Kind.EXIT -> Markup.EXIT)
9.70 + //}}}
9.71 + def is_raw(kind: Value) =
9.72 + kind == STDOUT
9.73 + def is_control(kind: Value) =
9.74 + kind == SYSTEM ||
9.75 + kind == SIGNAL ||
9.76 + kind == EXIT
9.77 + def is_system(kind: Value) =
9.78 + kind == SYSTEM ||
9.79 + kind == STDIN ||
9.80 + kind == SIGNAL ||
9.81 + kind == EXIT ||
9.82 + kind == STATUS
9.83 + }
9.84 +
9.85 + class Result(val kind: Kind.Value, val props: List[(String, String)], val result: String) {
9.86 + override def toString = {
9.87 + val trees = YXML.parse_body_failsafe(result)
9.88 + val res =
9.89 + if (kind == Kind.STATUS) trees.map(_.toString).mkString
9.90 + else trees.flatMap(XML.content(_).mkString).mkString
9.91 + if (props.isEmpty)
9.92 + kind.toString + " [[" + res + "]]"
9.93 + else
9.94 + kind.toString + " " +
9.95 + (for ((x, y) <- props) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
9.96 + }
9.97 + def is_raw = Kind.is_raw(kind)
9.98 + def is_control = Kind.is_control(kind)
9.99 + def is_system = Kind.is_system(kind)
9.100 + }
9.101 +
9.102 + def parse_message(isabelle_system: IsabelleSystem, result: Result) =
9.103 + {
9.104 + XML.Elem(Markup.MESSAGE, (Markup.CLASS, Kind.markup(result.kind)) :: result.props,
9.105 + YXML.parse_body_failsafe(isabelle_system.symbols.decode(result.result)))
9.106 + }
9.107 +}
9.108 +
9.109 +
9.110 +class IsabelleProcess(isabelle_system: IsabelleSystem,
9.111 + results: EventBus[IsabelleProcess.Result], args: String*)
9.112 +{
9.113 + import IsabelleProcess._
9.114 +
9.115 +
9.116 + /* demo constructor */
9.117 +
9.118 + def this(args: String*) =
9.119 + this(new IsabelleSystem, new EventBus[IsabelleProcess.Result] + Console.println, args: _*)
9.120 +
9.121 +
9.122 + /* process information */
9.123 +
9.124 + @volatile private var proc: Process = null
9.125 + @volatile private var closing = false
9.126 + @volatile private var pid: String = null
9.127 + @volatile private var the_session: String = null
9.128 + def session = the_session
9.129 +
9.130 +
9.131 + /* results */
9.132 +
9.133 + def parse_message(result: Result): XML.Tree =
9.134 + IsabelleProcess.parse_message(isabelle_system, result)
9.135 +
9.136 + private val result_queue = new LinkedBlockingQueue[Result]
9.137 +
9.138 + private def put_result(kind: Kind.Value, props: List[(String, String)], result: String)
9.139 + {
9.140 + if (kind == Kind.INIT) {
9.141 + val map = Map(props: _*)
9.142 + if (map.isDefinedAt(Markup.PID)) pid = map(Markup.PID)
9.143 + if (map.isDefinedAt(Markup.SESSION)) the_session = map(Markup.SESSION)
9.144 + }
9.145 + result_queue.put(new Result(kind, props, result))
9.146 + }
9.147 +
9.148 + private class ResultThread extends Thread("isabelle: results") {
9.149 + override def run() = {
9.150 + var finished = false
9.151 + while (!finished) {
9.152 + val result =
9.153 + try { result_queue.take }
9.154 + catch { case _: NullPointerException => null }
9.155 +
9.156 + if (result != null) {
9.157 + results.event(result)
9.158 + if (result.kind == Kind.EXIT) finished = true
9.159 + }
9.160 + else finished = true
9.161 + }
9.162 + }
9.163 + }
9.164 +
9.165 +
9.166 + /* signals */
9.167 +
9.168 + def interrupt() = synchronized {
9.169 + if (proc == null) error("Cannot interrupt Isabelle: no process")
9.170 + if (pid == null) put_result(Kind.SYSTEM, Nil, "Cannot interrupt: unknown pid")
9.171 + else {
9.172 + try {
9.173 + if (isabelle_system.execute(true, "kill", "-INT", pid).waitFor == 0)
9.174 + put_result(Kind.SIGNAL, Nil, "INT")
9.175 + else
9.176 + put_result(Kind.SYSTEM, Nil, "Cannot interrupt: kill command failed")
9.177 + }
9.178 + catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
9.179 + }
9.180 + }
9.181 +
9.182 + def kill() = synchronized {
9.183 + if (proc == 0) error("Cannot kill Isabelle: no process")
9.184 + else {
9.185 + try_close()
9.186 + Thread.sleep(500)
9.187 + put_result(Kind.SIGNAL, Nil, "KILL")
9.188 + proc.destroy
9.189 + proc = null
9.190 + pid = null
9.191 + }
9.192 + }
9.193 +
9.194 +
9.195 + /* output being piped into the process */
9.196 +
9.197 + private val output = new LinkedBlockingQueue[String]
9.198 +
9.199 + private def output_raw(text: String) = synchronized {
9.200 + if (proc == null) error("Cannot output to Isabelle: no process")
9.201 + if (closing) error("Cannot output to Isabelle: already closing")
9.202 + output.put(text)
9.203 + }
9.204 +
9.205 + def output_sync(text: String) =
9.206 + output_raw(" \\<^sync>\n; " + text + " \\<^sync>;\n")
9.207 +
9.208 +
9.209 + def command(text: String) =
9.210 + output_sync("Isabelle.command " + IsabelleSyntax.encode_string(text))
9.211 +
9.212 + def command(props: List[(String, String)], text: String) =
9.213 + output_sync("Isabelle.command " + IsabelleSyntax.encode_properties(props) + " " +
9.214 + IsabelleSyntax.encode_string(text))
9.215 +
9.216 + def ML(text: String) =
9.217 + output_sync("ML_val " + IsabelleSyntax.encode_string(text))
9.218 +
9.219 + def close() = synchronized { // FIXME watchdog/timeout
9.220 + output_raw("\u0000")
9.221 + closing = true
9.222 + }
9.223 +
9.224 + def try_close() = synchronized {
9.225 + if (proc != null && !closing) {
9.226 + try { close() }
9.227 + catch { case _: RuntimeException => }
9.228 + }
9.229 + }
9.230 +
9.231 +
9.232 + /* stdin */
9.233 +
9.234 + private class StdinThread(out_stream: OutputStream) extends Thread("isabelle: stdin") {
9.235 + override def run() = {
9.236 + val writer = new BufferedWriter(new OutputStreamWriter(out_stream, isabelle_system.charset))
9.237 + var finished = false
9.238 + while (!finished) {
9.239 + try {
9.240 + //{{{
9.241 + val s = output.take
9.242 + if (s == "\u0000") {
9.243 + writer.close
9.244 + finished = true
9.245 + }
9.246 + else {
9.247 + put_result(Kind.STDIN, Nil, s)
9.248 + writer.write(s)
9.249 + writer.flush
9.250 + }
9.251 + //}}}
9.252 + }
9.253 + catch {
9.254 + case e: IOException => put_result(Kind.SYSTEM, Nil, "Stdin thread: " + e.getMessage)
9.255 + }
9.256 + }
9.257 + put_result(Kind.SYSTEM, Nil, "Stdin thread terminated")
9.258 + }
9.259 + }
9.260 +
9.261 +
9.262 + /* stdout */
9.263 +
9.264 + private class StdoutThread(in_stream: InputStream) extends Thread("isabelle: stdout") {
9.265 + override def run() = {
9.266 + val reader = new BufferedReader(new InputStreamReader(in_stream, isabelle_system.charset))
9.267 + var result = new StringBuilder(100)
9.268 +
9.269 + var finished = false
9.270 + while (!finished) {
9.271 + try {
9.272 + //{{{
9.273 + var c = -1
9.274 + var done = false
9.275 + while (!done && (result.length == 0 || reader.ready)) {
9.276 + c = reader.read
9.277 + if (c >= 0) result.append(c.asInstanceOf[Char])
9.278 + else done = true
9.279 + }
9.280 + if (result.length > 0) {
9.281 + put_result(Kind.STDOUT, Nil, result.toString)
9.282 + result.length = 0
9.283 + }
9.284 + else {
9.285 + reader.close
9.286 + finished = true
9.287 + try_close()
9.288 + }
9.289 + //}}}
9.290 + }
9.291 + catch {
9.292 + case e: IOException => put_result(Kind.SYSTEM, Nil, "Stdout thread: " + e.getMessage)
9.293 + }
9.294 + }
9.295 + put_result(Kind.SYSTEM, Nil, "Stdout thread terminated")
9.296 + }
9.297 + }
9.298 +
9.299 +
9.300 + /* messages */
9.301 +
9.302 + private class MessageThread(fifo: String) extends Thread("isabelle: messages") {
9.303 + override def run() = {
9.304 + val reader = isabelle_system.fifo_reader(fifo)
9.305 + var kind: Kind.Value = null
9.306 + var props: List[(String, String)] = Nil
9.307 + var result = new StringBuilder
9.308 +
9.309 + var finished = false
9.310 + while (!finished) {
9.311 + try {
9.312 + if (kind == null) {
9.313 + //{{{ Char mode -- resync
9.314 + var c = -1
9.315 + do {
9.316 + c = reader.read
9.317 + if (c >= 0 && c != 2) result.append(c.asInstanceOf[Char])
9.318 + } while (c >= 0 && c != 2)
9.319 +
9.320 + if (result.length > 0) {
9.321 + put_result(Kind.SYSTEM, Nil, "Malformed message:\n" + result.toString)
9.322 + result.length = 0
9.323 + }
9.324 + if (c < 0) {
9.325 + reader.close
9.326 + finished = true
9.327 + try_close()
9.328 + }
9.329 + else {
9.330 + c = reader.read
9.331 + if (Kind.code.isDefinedAt(c)) kind = Kind.code(c)
9.332 + else kind = null
9.333 + }
9.334 + //}}}
9.335 + }
9.336 + else {
9.337 + //{{{ Line mode
9.338 + val line = reader.readLine
9.339 + if (line == null) {
9.340 + reader.close
9.341 + finished = true
9.342 + try_close()
9.343 + }
9.344 + else {
9.345 + val len = line.length
9.346 + // property
9.347 + if (line.endsWith("\u0002,")) {
9.348 + val i = line.indexOf('=')
9.349 + if (i > 0) {
9.350 + val name = line.substring(0, i)
9.351 + val value = line.substring(i + 1, len - 2)
9.352 + props = (name, value) :: props
9.353 + }
9.354 + }
9.355 + // last text line
9.356 + else if (line.endsWith("\u0002.")) {
9.357 + result.append(line.substring(0, len - 2))
9.358 + put_result(kind, props.reverse, result.toString)
9.359 + kind = null
9.360 + props = Nil
9.361 + result.length = 0
9.362 + }
9.363 + // text line
9.364 + else {
9.365 + result.append(line)
9.366 + result.append('\n')
9.367 + }
9.368 + }
9.369 + //}}}
9.370 + }
9.371 + }
9.372 + catch {
9.373 + case e: IOException => put_result(Kind.SYSTEM, Nil, "Message thread: " + e.getMessage)
9.374 + }
9.375 + }
9.376 + put_result(Kind.SYSTEM, Nil, "Message thread terminated")
9.377 + }
9.378 + }
9.379 +
9.380 +
9.381 +
9.382 + /** main **/
9.383 +
9.384 + {
9.385 + /* isabelle version */
9.386 +
9.387 + {
9.388 + val (msg, rc) = isabelle_system.isabelle_tool("version")
9.389 + if (rc != 0) error("Version check failed -- bad Isabelle installation:\n" + msg)
9.390 + put_result(Kind.SYSTEM, Nil, msg)
9.391 + }
9.392 +
9.393 +
9.394 + /* messages */
9.395 +
9.396 + val message_fifo = isabelle_system.mk_fifo()
9.397 + def rm_fifo() = isabelle_system.rm_fifo(message_fifo)
9.398 +
9.399 + val message_thread = new MessageThread(message_fifo)
9.400 + message_thread.start
9.401 +
9.402 + new ResultThread().start
9.403 +
9.404 +
9.405 + /* exec process */
9.406 +
9.407 + try {
9.408 + val cmdline =
9.409 + List(isabelle_system.getenv_strict("ISABELLE_PROCESS"), "-W", message_fifo) ++ args
9.410 + proc = isabelle_system.execute(true, cmdline: _*)
9.411 + }
9.412 + catch {
9.413 + case e: IOException =>
9.414 + rm_fifo()
9.415 + error("Failed to execute Isabelle process: " + e.getMessage)
9.416 + }
9.417 +
9.418 +
9.419 + /* stdin/stdout */
9.420 +
9.421 + new StdinThread(proc.getOutputStream).start
9.422 + new StdoutThread(proc.getInputStream).start
9.423 +
9.424 +
9.425 + /* exit */
9.426 +
9.427 + new Thread("isabelle: exit") {
9.428 + override def run() = {
9.429 + val rc = proc.waitFor()
9.430 + Thread.sleep(300)
9.431 + put_result(Kind.SYSTEM, Nil, "Exit thread terminated")
9.432 + put_result(Kind.EXIT, Nil, Integer.toString(rc))
9.433 + rm_fifo()
9.434 + }
9.435 + }.start
9.436 +
9.437 + }
9.438 +}
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/src/Pure/System/isar.ML Sat Feb 28 18:00:20 2009 +0100
10.3 @@ -0,0 +1,415 @@
10.4 +(* Title: Pure/Isar/isar.ML
10.5 + Author: Makarius
10.6 +
10.7 +The global Isabelle/Isar state and main read-eval-print loop.
10.8 +*)
10.9 +
10.10 +signature ISAR =
10.11 +sig
10.12 + val init: unit -> unit
10.13 + val exn: unit -> (exn * string) option
10.14 + val state: unit -> Toplevel.state
10.15 + val context: unit -> Proof.context
10.16 + val goal: unit -> thm
10.17 + val print: unit -> unit
10.18 + val >> : Toplevel.transition -> bool
10.19 + val >>> : Toplevel.transition list -> unit
10.20 + val linear_undo: int -> unit
10.21 + val undo: int -> unit
10.22 + val kill: unit -> unit
10.23 + val kill_proof: unit -> unit
10.24 + val crashes: exn list ref
10.25 + val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
10.26 + val loop: unit -> unit
10.27 + val main: unit -> unit
10.28 +
10.29 + type id = string
10.30 + val no_id: id
10.31 + val create_command: Toplevel.transition -> id
10.32 + val insert_command: id -> id -> unit
10.33 + val remove_command: id -> unit
10.34 +end;
10.35 +
10.36 +structure Isar: ISAR =
10.37 +struct
10.38 +
10.39 +
10.40 +(** TTY model -- SINGLE-THREADED! **)
10.41 +
10.42 +(* the global state *)
10.43 +
10.44 +type history = (Toplevel.state * Toplevel.transition) list;
10.45 + (*previous state, state transition -- regular commands only*)
10.46 +
10.47 +local
10.48 + val global_history = ref ([]: history);
10.49 + val global_state = ref Toplevel.toplevel;
10.50 + val global_exn = ref (NONE: (exn * string) option);
10.51 +in
10.52 +
10.53 +fun edit_history count f = NAMED_CRITICAL "Isar" (fn () =>
10.54 + let
10.55 + fun edit 0 (st, hist) = (global_history := hist; global_state := st; global_exn := NONE)
10.56 + | edit n (st, hist) = edit (n - 1) (f st hist);
10.57 + in edit count (! global_state, ! global_history) end);
10.58 +
10.59 +fun state () = NAMED_CRITICAL "Isar" (fn () => ! global_state);
10.60 +fun set_state state = NAMED_CRITICAL "Isar" (fn () => global_state := state);
10.61 +
10.62 +fun exn () = NAMED_CRITICAL "Isar" (fn () => ! global_exn);
10.63 +fun set_exn exn = NAMED_CRITICAL "Isar" (fn () => global_exn := exn);
10.64 +
10.65 +end;
10.66 +
10.67 +
10.68 +fun init () = edit_history 1 (K (K (Toplevel.toplevel, [])));
10.69 +
10.70 +fun context () = Toplevel.context_of (state ())
10.71 + handle Toplevel.UNDEF => error "Unknown context";
10.72 +
10.73 +fun goal () = #2 (#2 (Proof.get_goal (Toplevel.proof_of (state ()))))
10.74 + handle Toplevel.UNDEF => error "No goal present";
10.75 +
10.76 +fun print () = Toplevel.print_state false (state ());
10.77 +
10.78 +
10.79 +(* history navigation *)
10.80 +
10.81 +local
10.82 +
10.83 +fun find_and_undo _ [] = error "Undo history exhausted"
10.84 + | find_and_undo which ((prev, tr) :: hist) =
10.85 + ((case Toplevel.init_of tr of SOME name => ThyInfo.kill_thy name | NONE => ());
10.86 + if which (Toplevel.name_of tr) then (prev, hist) else find_and_undo which hist);
10.87 +
10.88 +in
10.89 +
10.90 +fun linear_undo n = edit_history n (K (find_and_undo (K true)));
10.91 +
10.92 +fun undo n = edit_history n (fn st => fn hist =>
10.93 + find_and_undo (if Toplevel.is_proof st then K true else OuterKeyword.is_theory) hist);
10.94 +
10.95 +fun kill () = edit_history 1 (fn st => fn hist =>
10.96 + find_and_undo
10.97 + (if Toplevel.is_proof st then OuterKeyword.is_theory else OuterKeyword.is_theory_begin) hist);
10.98 +
10.99 +fun kill_proof () = edit_history 1 (fn st => fn hist =>
10.100 + if Toplevel.is_proof st then find_and_undo OuterKeyword.is_theory hist
10.101 + else raise Toplevel.UNDEF);
10.102 +
10.103 +end;
10.104 +
10.105 +
10.106 +(* interactive state transformations *)
10.107 +
10.108 +fun op >> tr =
10.109 + (case Toplevel.transition true tr (state ()) of
10.110 + NONE => false
10.111 + | SOME (_, SOME err) => (set_exn (SOME err); Toplevel.error_msg tr err; true)
10.112 + | SOME (st', NONE) =>
10.113 + let
10.114 + val name = Toplevel.name_of tr;
10.115 + val _ = if OuterKeyword.is_theory_begin name then init () else ();
10.116 + val _ =
10.117 + if OuterKeyword.is_regular name
10.118 + then edit_history 1 (fn st => fn hist => (st', (st, tr) :: hist)) else ();
10.119 + in true end);
10.120 +
10.121 +fun op >>> [] = ()
10.122 + | op >>> (tr :: trs) = if op >> tr then op >>> trs else ();
10.123 +
10.124 +
10.125 +(* toplevel loop *)
10.126 +
10.127 +val crashes = ref ([]: exn list);
10.128 +
10.129 +local
10.130 +
10.131 +fun raw_loop secure src =
10.132 + let
10.133 + fun check_secure () =
10.134 + (if secure then warning "Secure loop -- cannot exit to ML" else (); secure);
10.135 + in
10.136 + (case Source.get_single (Source.set_prompt Source.default_prompt src) of
10.137 + NONE => if secure then quit () else ()
10.138 + | SOME (tr, src') => if op >> tr orelse check_secure () then raw_loop secure src' else ())
10.139 + handle exn =>
10.140 + (Output.error_msg (Toplevel.exn_message exn)
10.141 + handle crash =>
10.142 + (CRITICAL (fn () => change crashes (cons crash));
10.143 + warning "Recovering from Isar toplevel crash -- see also Isar.crashes");
10.144 + raw_loop secure src)
10.145 + end;
10.146 +
10.147 +in
10.148 +
10.149 +fun toplevel_loop {init = do_init, welcome, sync, secure} =
10.150 + (Context.set_thread_data NONE;
10.151 + if do_init then init () else (); (* FIXME init editor model *)
10.152 + if welcome then writeln (Session.welcome ()) else ();
10.153 + uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ());
10.154 +
10.155 +end;
10.156 +
10.157 +fun loop () =
10.158 + toplevel_loop {init = false, welcome = false, sync = false, secure = Secure.is_secure ()};
10.159 +
10.160 +fun main () =
10.161 + toplevel_loop {init = true, welcome = true, sync = false, secure = Secure.is_secure ()};
10.162 +
10.163 +
10.164 +
10.165 +(** individual toplevel commands **)
10.166 +
10.167 +(* unique identification *)
10.168 +
10.169 +type id = string;
10.170 +val no_id : id = "";
10.171 +
10.172 +
10.173 +(* command category *)
10.174 +
10.175 +datatype category = Empty | Theory | Proof | Diag | Control;
10.176 +
10.177 +fun category_of tr =
10.178 + let val name = Toplevel.name_of tr in
10.179 + if name = "" then Empty
10.180 + else if OuterKeyword.is_theory name then Theory
10.181 + else if OuterKeyword.is_proof name then Proof
10.182 + else if OuterKeyword.is_diag name then Diag
10.183 + else Control
10.184 + end;
10.185 +
10.186 +val is_theory = fn Theory => true | _ => false;
10.187 +val is_proper = fn Theory => true | Proof => true | _ => false;
10.188 +val is_regular = fn Control => false | _ => true;
10.189 +
10.190 +
10.191 +(* command status *)
10.192 +
10.193 +datatype status =
10.194 + Unprocessed |
10.195 + Running |
10.196 + Failed of exn * string |
10.197 + Finished of Toplevel.state;
10.198 +
10.199 +fun status_markup Unprocessed = Markup.unprocessed
10.200 + | status_markup Running = (Markup.runningN, [])
10.201 + | status_markup (Failed _) = Markup.failed
10.202 + | status_markup (Finished _) = Markup.finished;
10.203 +
10.204 +fun run int tr state =
10.205 + (case Toplevel.transition int tr state of
10.206 + NONE => NONE
10.207 + | SOME (_, SOME err) => (Toplevel.error_msg tr err; SOME (Failed err))
10.208 + | SOME (state', NONE) => SOME (Finished state'));
10.209 +
10.210 +
10.211 +(* datatype command *)
10.212 +
10.213 +datatype command = Command of
10.214 + {category: category,
10.215 + transition: Toplevel.transition,
10.216 + status: status};
10.217 +
10.218 +fun make_command (category, transition, status) =
10.219 + Command {category = category, transition = transition, status = status};
10.220 +
10.221 +val empty_command =
10.222 + make_command (Empty, Toplevel.empty, Finished Toplevel.toplevel);
10.223 +
10.224 +fun map_command f (Command {category, transition, status}) =
10.225 + make_command (f (category, transition, status));
10.226 +
10.227 +fun map_status f = map_command (fn (category, transition, status) =>
10.228 + (category, transition, f status));
10.229 +
10.230 +
10.231 +(* global collection of identified commands *)
10.232 +
10.233 +fun err_dup id = sys_error ("Duplicate command " ^ quote id);
10.234 +fun err_undef id = sys_error ("Unknown command " ^ quote id);
10.235 +
10.236 +local val global_commands = ref (Graph.empty: command Graph.T) in
10.237 +
10.238 +fun change_commands f = NAMED_CRITICAL "Isar" (fn () => change global_commands f)
10.239 + handle Graph.DUP bad => err_dup bad | Graph.UNDEF bad => err_undef bad;
10.240 +
10.241 +fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands);
10.242 +
10.243 +end;
10.244 +
10.245 +fun add_edge (id1, id2) =
10.246 + if id1 = no_id orelse id2 = no_id then I else Graph.add_edge (id1, id2);
10.247 +
10.248 +
10.249 +fun init_commands () = change_commands (K Graph.empty);
10.250 +
10.251 +fun the_command id =
10.252 + let val Command cmd =
10.253 + if id = no_id then empty_command
10.254 + else (Graph.get_node (get_commands ()) id handle Graph.UNDEF bad => err_undef bad)
10.255 + in cmd end;
10.256 +
10.257 +fun prev_command id =
10.258 + if id = no_id then no_id
10.259 + else
10.260 + (case Graph.imm_preds (get_commands ()) id handle Graph.UNDEF bad => err_undef bad of
10.261 + [] => no_id
10.262 + | [prev] => prev
10.263 + | _ => sys_error ("Non-linear command dependency " ^ quote id));
10.264 +
10.265 +fun next_commands id =
10.266 + if id = no_id then []
10.267 + else Graph.imm_succs (get_commands ()) id handle Graph.UNDEF bad => err_undef bad;
10.268 +
10.269 +fun descendant_commands ids =
10.270 + Graph.all_succs (get_commands ()) (distinct (op =) (filter_out (fn id => id = no_id) ids))
10.271 + handle Graph.UNDEF bad => err_undef bad;
10.272 +
10.273 +
10.274 +(* maintain status *)
10.275 +
10.276 +fun report_status markup id = Toplevel.status (#transition (the_command id)) markup;
10.277 +
10.278 +fun update_status status id = change_commands (Graph.map_node id (map_status (K status)));
10.279 +
10.280 +fun report_update_status status id =
10.281 + change_commands (Graph.map_node id (map_status (fn old_status =>
10.282 + let val markup = status_markup status
10.283 + in if markup <> status_markup old_status then report_status markup id else (); status end)));
10.284 +
10.285 +
10.286 +(* create and dispose commands *)
10.287 +
10.288 +fun create_command raw_tr =
10.289 + let
10.290 + val (id, tr) =
10.291 + (case Toplevel.get_id raw_tr of
10.292 + SOME id => (id, raw_tr)
10.293 + | NONE =>
10.294 + let val id =
10.295 + if ! Toplevel.debug then "isabelle:" ^ Toplevel.name_of raw_tr ^ serial_string ()
10.296 + else "isabelle:" ^ serial_string ()
10.297 + in (id, Toplevel.put_id id raw_tr) end);
10.298 +
10.299 + val cmd = make_command (category_of tr, tr, Unprocessed);
10.300 + val _ = change_commands (Graph.new_node (id, cmd));
10.301 + in id end;
10.302 +
10.303 +fun dispose_commands ids =
10.304 + let
10.305 + val desc = descendant_commands ids;
10.306 + val _ = List.app (report_status Markup.disposed) desc;
10.307 + val _ = change_commands (Graph.del_nodes desc);
10.308 + in () end;
10.309 +
10.310 +
10.311 +(* final state *)
10.312 +
10.313 +fun the_state id =
10.314 + (case the_command id of
10.315 + {status = Finished state, ...} => state
10.316 + | {transition, ...} => error ("Unfinished command " ^ Toplevel.str_of transition));
10.317 +
10.318 +
10.319 +
10.320 +(** editor model **)
10.321 +
10.322 +(* run commands *)
10.323 +
10.324 +fun try_run id =
10.325 + (case try the_state (prev_command id) of
10.326 + NONE => ()
10.327 + | SOME state =>
10.328 + (case run true (#transition (the_command id)) state of
10.329 + NONE => ()
10.330 + | SOME status => report_update_status status id));
10.331 +
10.332 +fun rerun_commands ids =
10.333 + (List.app (report_update_status Unprocessed) ids; List.app try_run ids);
10.334 +
10.335 +
10.336 +(* modify document *)
10.337 +
10.338 +fun insert_command prev id = NAMED_CRITICAL "Isar" (fn () =>
10.339 + let
10.340 + val nexts = next_commands prev;
10.341 + val _ = change_commands
10.342 + (fold (fn next => Graph.del_edge (prev, next)) nexts #> add_edge (prev, id) #>
10.343 + fold (fn next => Graph.add_edge (id, next)) nexts);
10.344 + in descendant_commands [id] end) |> rerun_commands;
10.345 +
10.346 +fun remove_command id = NAMED_CRITICAL "Isar" (fn () =>
10.347 + let
10.348 + val prev = prev_command id;
10.349 + val nexts = next_commands id;
10.350 + val _ = change_commands
10.351 + (fold (fn next => Graph.del_edge (id, next)) nexts #>
10.352 + fold (fn next => add_edge (prev, next)) nexts);
10.353 + in descendant_commands nexts end) |> rerun_commands;
10.354 +
10.355 +
10.356 +
10.357 +(** command syntax **)
10.358 +
10.359 +local
10.360 +
10.361 +structure P = OuterParse and K = OuterKeyword;
10.362 +val op >> = Scan.>>;
10.363 +
10.364 +in
10.365 +
10.366 +(* global history *)
10.367 +
10.368 +val _ =
10.369 + OuterSyntax.improper_command "init_toplevel" "init toplevel point-of-interest" K.control
10.370 + (Scan.succeed (Toplevel.no_timing o Toplevel.imperative init));
10.371 +
10.372 +val _ =
10.373 + OuterSyntax.improper_command "linear_undo" "undo commands" K.control
10.374 + (Scan.optional P.nat 1 >>
10.375 + (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => linear_undo n)));
10.376 +
10.377 +val _ =
10.378 + OuterSyntax.improper_command "undo" "undo commands (skipping closed proofs)" K.control
10.379 + (Scan.optional P.nat 1 >>
10.380 + (fn n => Toplevel.no_timing o Toplevel.imperative (fn () => undo n)));
10.381 +
10.382 +val _ =
10.383 + OuterSyntax.improper_command "undos_proof" "undo commands (skipping closed proofs)" K.control
10.384 + (Scan.optional P.nat 1 >> (fn n => Toplevel.no_timing o
10.385 + Toplevel.keep (fn state =>
10.386 + if Toplevel.is_proof state then (undo n; print ()) else raise Toplevel.UNDEF)));
10.387 +
10.388 +val _ =
10.389 + OuterSyntax.improper_command "cannot_undo" "partial undo -- Proof General legacy" K.control
10.390 + (P.name >>
10.391 + (fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => undo 1)
10.392 + | txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
10.393 +
10.394 +val _ =
10.395 + OuterSyntax.improper_command "kill" "kill partial proof or theory development" K.control
10.396 + (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
10.397 +
10.398 +
10.399 +(* editor model *)
10.400 +
10.401 +val _ =
10.402 + OuterSyntax.internal_command "Isar.command"
10.403 + (P.string -- P.string >> (fn (id, text) =>
10.404 + Toplevel.imperative (fn () =>
10.405 + ignore (create_command (OuterSyntax.prepare_command (Position.id id) text)))));
10.406 +
10.407 +val _ =
10.408 + OuterSyntax.internal_command "Isar.insert"
10.409 + (P.string -- P.string >> (fn (prev, id) =>
10.410 + Toplevel.imperative (fn () => insert_command prev id)));
10.411 +
10.412 +val _ =
10.413 + OuterSyntax.internal_command "Isar.remove"
10.414 + (P.string >> (fn id => Toplevel.imperative (fn () => remove_command id)));
10.415 +
10.416 +end;
10.417 +
10.418 +end;
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/src/Pure/System/session.ML Sat Feb 28 18:00:20 2009 +0100
11.3 @@ -0,0 +1,112 @@
11.4 +(* Title: Pure/System/session.ML
11.5 + Author: Markus Wenzel, TU Muenchen
11.6 +
11.7 +Session management -- maintain state of logic images.
11.8 +*)
11.9 +
11.10 +signature SESSION =
11.11 +sig
11.12 + val id: unit -> string list
11.13 + val name: unit -> string
11.14 + val welcome: unit -> string
11.15 + val use_dir: string -> bool -> string list -> bool -> bool -> string -> bool -> string list ->
11.16 + string -> string -> bool * string -> string -> int -> bool -> int -> int -> bool -> unit
11.17 + val finish: unit -> unit
11.18 +end;
11.19 +
11.20 +structure Session: SESSION =
11.21 +struct
11.22 +
11.23 +
11.24 +(* session state *)
11.25 +
11.26 +val session = ref ([Context.PureN]: string list);
11.27 +val session_path = ref ([]: string list);
11.28 +val session_finished = ref false;
11.29 +val remote_path = ref (NONE: Url.T option);
11.30 +
11.31 +
11.32 +(* access path *)
11.33 +
11.34 +fun id () = ! session;
11.35 +fun path () = ! session_path;
11.36 +
11.37 +fun str_of [] = Context.PureN
11.38 + | str_of elems = space_implode "/" elems;
11.39 +
11.40 +fun name () = "Isabelle/" ^ str_of (path ());
11.41 +
11.42 +
11.43 +(* welcome *)
11.44 +
11.45 +fun welcome () =
11.46 + if Distribution.is_official then
11.47 + "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
11.48 + else
11.49 + "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")" ^
11.50 + (if Distribution.changelog <> "" then "\nSee also " ^ Distribution.changelog else "");
11.51 +
11.52 +val _ =
11.53 + OuterSyntax.improper_command "welcome" "print welcome message" OuterKeyword.diag
11.54 + (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (writeln o welcome)));
11.55 +
11.56 +
11.57 +(* add_path *)
11.58 +
11.59 +fun add_path reset s =
11.60 + let val sess = ! session @ [s] in
11.61 + (case duplicates (op =) sess of
11.62 + [] => (session := sess; session_path := ((if reset then [] else ! session_path) @ [s]))
11.63 + | dups => error ("Duplicate session identifiers " ^ commas_quote dups ^ " in " ^ str_of sess))
11.64 + end;
11.65 +
11.66 +
11.67 +(* init *)
11.68 +
11.69 +fun init reset parent name =
11.70 + if not (member (op =) (! session) parent) orelse not (! session_finished) then
11.71 + error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
11.72 + else (add_path reset name; session_finished := false);
11.73 +
11.74 +
11.75 +(* finish *)
11.76 +
11.77 +fun finish () =
11.78 + (Output.accumulated_time ();
11.79 + ThyInfo.finish ();
11.80 + Present.finish ();
11.81 + Future.shutdown ();
11.82 + session_finished := true);
11.83 +
11.84 +
11.85 +(* use_dir *)
11.86 +
11.87 +fun get_rpath rpath =
11.88 + (if rpath = "" then () else
11.89 + if is_some (! remote_path) then
11.90 + error "Path for remote theory browsing information may only be set once"
11.91 + else
11.92 + remote_path := SOME (Url.explode rpath);
11.93 + (! remote_path, rpath <> ""));
11.94 +
11.95 +fun dumping (_, "") = NONE
11.96 + | dumping (cp, path) = SOME (cp, Path.explode path);
11.97 +
11.98 +fun use_dir root build modes reset info doc doc_graph doc_versions
11.99 + parent name dump rpath level verbose max_threads trace_threads parallel_proofs =
11.100 + ((fn () =>
11.101 + (init reset parent name;
11.102 + Present.init build info doc doc_graph doc_versions (path ()) name
11.103 + (dumping dump) (get_rpath rpath) verbose (map ThyInfo.get_theory (ThyInfo.get_names ()));
11.104 + use root;
11.105 + finish ()))
11.106 + |> setmp_noncritical Proofterm.proofs level
11.107 + |> setmp_noncritical print_mode (modes @ print_mode_value ())
11.108 + |> setmp_noncritical Goal.parallel_proofs parallel_proofs
11.109 + |> setmp_noncritical Multithreading.trace trace_threads
11.110 + |> setmp_noncritical Multithreading.max_threads
11.111 + (if Multithreading.available then max_threads
11.112 + else (if max_threads = 1 then () else warning "Multithreading support unavailable"; 1))) ()
11.113 + handle exn => (Output.error_msg (Toplevel.exn_message exn); exit 1);
11.114 +
11.115 +end;
12.1 --- a/src/Pure/Tools/ROOT.ML Sat Feb 28 17:09:32 2009 +0100
12.2 +++ b/src/Pure/Tools/ROOT.ML Sat Feb 28 18:00:20 2009 +0100
12.3 @@ -4,7 +4,6 @@
12.4 *)
12.5
12.6 use "named_thms.ML";
12.7 -use "isabelle_process.ML";
12.8
12.9 (*basic XML support*)
12.10 use "xml_syntax.ML";
13.1 --- a/src/Pure/Tools/isabelle_process.ML Sat Feb 28 17:09:32 2009 +0100
13.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
13.3 @@ -1,138 +0,0 @@
13.4 -(* Title: Pure/Tools/isabelle_process.ML
13.5 - Author: Makarius
13.6 -
13.7 -Isabelle process wrapper -- interaction via external program.
13.8 -
13.9 -General format of process output:
13.10 -
13.11 - (1) unmarked stdout/stderr, no line structure (output should be
13.12 - processed immediately as it arrives);
13.13 -
13.14 - (2) properly marked-up messages, e.g. for writeln channel
13.15 -
13.16 - "\002A" ^ props ^ "\002,\n" ^ text ^ "\002.\n"
13.17 -
13.18 - where the props consist of name=value lines terminated by "\002,\n"
13.19 - each, and the remaining text is any number of lines (output is
13.20 - supposed to be processed in one piece);
13.21 -
13.22 - (3) special init message holds "pid" and "session" property;
13.23 -
13.24 - (4) message content is encoded in YXML format.
13.25 -*)
13.26 -
13.27 -signature ISABELLE_PROCESS =
13.28 -sig
13.29 - val isabelle_processN: string
13.30 - val init: string -> unit
13.31 -end;
13.32 -
13.33 -structure IsabelleProcess: ISABELLE_PROCESS =
13.34 -struct
13.35 -
13.36 -(* print modes *)
13.37 -
13.38 -val isabelle_processN = "isabelle_process";
13.39 -
13.40 -val _ = Output.add_mode isabelle_processN Output.default_output Output.default_escape;
13.41 -val _ = Markup.add_mode isabelle_processN YXML.output_markup;
13.42 -
13.43 -
13.44 -(* message markup *)
13.45 -
13.46 -fun special ch = Symbol.STX ^ ch;
13.47 -val special_sep = special ",";
13.48 -val special_end = special ".";
13.49 -
13.50 -local
13.51 -
13.52 -fun clean_string bad str =
13.53 - if exists_string (member (op =) bad) str then
13.54 - translate_string (fn c => if member (op =) bad c then Symbol.DEL else c) str
13.55 - else str;
13.56 -
13.57 -fun message_props props =
13.58 - let val clean = clean_string [Symbol.STX, "\n", "\r"]
13.59 - in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end;
13.60 -
13.61 -fun message_pos trees = trees |> get_first
13.62 - (fn XML.Elem (name, atts, ts) =>
13.63 - if name = Markup.positionN then SOME (Position.of_properties atts)
13.64 - else message_pos ts
13.65 - | _ => NONE);
13.66 -
13.67 -fun output out_stream s = NAMED_CRITICAL "IO" (fn () =>
13.68 - (TextIO.output (out_stream, s); TextIO.output (out_stream, "\n")));
13.69 -
13.70 -in
13.71 -
13.72 -fun message _ _ "" = ()
13.73 - | message out_stream ch body =
13.74 - let
13.75 - val pos = the_default Position.none (message_pos (YXML.parse_body body));
13.76 - val props =
13.77 - Position.properties_of (Position.thread_data ())
13.78 - |> Position.default_properties pos;
13.79 - val txt = clean_string [Symbol.STX] body;
13.80 - in output out_stream (special ch ^ message_props props ^ txt ^ special_end) end;
13.81 -
13.82 -fun init_message out_stream =
13.83 - let
13.84 - val pid = (Markup.pidN, process_id ());
13.85 - val session = (Markup.sessionN, List.last (Session.id ()) handle List.Empty => "unknown");
13.86 - val text = Session.welcome ();
13.87 - in output out_stream (special "A" ^ message_props [pid, session] ^ text ^ special_end) end;
13.88 -
13.89 -end;
13.90 -
13.91 -
13.92 -(* channels *)
13.93 -
13.94 -local
13.95 -
13.96 -fun auto_flush stream =
13.97 - let
13.98 - val _ = TextIO.StreamIO.setBufferMode (TextIO.getOutstream stream, IO.BLOCK_BUF);
13.99 - fun loop () =
13.100 - (OS.Process.sleep (Time.fromMilliseconds 50); try TextIO.flushOut stream; loop ());
13.101 - in loop end;
13.102 -
13.103 -in
13.104 -
13.105 -fun setup_channels out =
13.106 - let
13.107 - val out_stream =
13.108 - if out = "-" then TextIO.stdOut
13.109 - else
13.110 - let
13.111 - val path = File.platform_path (Path.explode out);
13.112 - val out_stream = TextIO.openOut path; (*fifo blocks until reader is ready*)
13.113 - val _ = OS.FileSys.remove path; (*prevent alien access, indicate writer is ready*)
13.114 - val _ = SimpleThread.fork false (auto_flush TextIO.stdOut);
13.115 - in out_stream end;
13.116 - val _ = SimpleThread.fork false (auto_flush out_stream);
13.117 - val _ = SimpleThread.fork false (auto_flush TextIO.stdErr);
13.118 - in
13.119 - Output.status_fn := message out_stream "B";
13.120 - Output.writeln_fn := message out_stream "C";
13.121 - Output.priority_fn := message out_stream "D";
13.122 - Output.tracing_fn := message out_stream "E";
13.123 - Output.warning_fn := message out_stream "F";
13.124 - Output.error_fn := message out_stream "G";
13.125 - Output.debug_fn := message out_stream "H";
13.126 - Output.prompt_fn := ignore;
13.127 - out_stream
13.128 - end;
13.129 -
13.130 -end;
13.131 -
13.132 -
13.133 -(* init *)
13.134 -
13.135 -fun init out =
13.136 - (change print_mode (update (op =) isabelle_processN);
13.137 - setup_channels out |> init_message;
13.138 - OuterKeyword.report ();
13.139 - Isar.toplevel_loop {init = true, welcome = false, sync = true, secure = true});
13.140 -
13.141 -end;
14.1 --- a/src/Pure/Tools/isabelle_process.scala Sat Feb 28 17:09:32 2009 +0100
14.2 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000
14.3 @@ -1,435 +0,0 @@
14.4 -/* Title: Pure/Tools/isabelle_process.ML
14.5 - Author: Makarius
14.6 - Options: :folding=explicit:collapseFolds=1:
14.7 -
14.8 -Isabelle process management -- always reactive due to multi-threaded I/O.
14.9 -*/
14.10 -
14.11 -package isabelle
14.12 -
14.13 -import java.util.concurrent.LinkedBlockingQueue
14.14 -import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter,
14.15 - InputStream, OutputStream, IOException}
14.16 -
14.17 -
14.18 -object IsabelleProcess {
14.19 -
14.20 - /* results */
14.21 -
14.22 - object Kind extends Enumeration {
14.23 - //{{{ values and codes
14.24 - // internal system notification
14.25 - val SYSTEM = Value("SYSTEM")
14.26 - // Posix channels/events
14.27 - val STDIN = Value("STDIN")
14.28 - val STDOUT = Value("STDOUT")
14.29 - val SIGNAL = Value("SIGNAL")
14.30 - val EXIT = Value("EXIT")
14.31 - // Isabelle messages
14.32 - val INIT = Value("INIT")
14.33 - val STATUS = Value("STATUS")
14.34 - val WRITELN = Value("WRITELN")
14.35 - val PRIORITY = Value("PRIORITY")
14.36 - val TRACING = Value("TRACING")
14.37 - val WARNING = Value("WARNING")
14.38 - val ERROR = Value("ERROR")
14.39 - val DEBUG = Value("DEBUG")
14.40 - // messages codes
14.41 - val code = Map(
14.42 - ('A' : Int) -> Kind.INIT,
14.43 - ('B' : Int) -> Kind.STATUS,
14.44 - ('C' : Int) -> Kind.WRITELN,
14.45 - ('D' : Int) -> Kind.PRIORITY,
14.46 - ('E' : Int) -> Kind.TRACING,
14.47 - ('F' : Int) -> Kind.WARNING,
14.48 - ('G' : Int) -> Kind.ERROR,
14.49 - ('H' : Int) -> Kind.DEBUG,
14.50 - ('0' : Int) -> Kind.SYSTEM,
14.51 - ('1' : Int) -> Kind.STDIN,
14.52 - ('2' : Int) -> Kind.STDOUT,
14.53 - ('3' : Int) -> Kind.SIGNAL,
14.54 - ('4' : Int) -> Kind.EXIT)
14.55 - // message markup
14.56 - val markup = Map(
14.57 - Kind.INIT -> Markup.INIT,
14.58 - Kind.STATUS -> Markup.STATUS,
14.59 - Kind.WRITELN -> Markup.WRITELN,
14.60 - Kind.PRIORITY -> Markup.PRIORITY,
14.61 - Kind.TRACING -> Markup.TRACING,
14.62 - Kind.WARNING -> Markup.WARNING,
14.63 - Kind.ERROR -> Markup.ERROR,
14.64 - Kind.DEBUG -> Markup.DEBUG,
14.65 - Kind.SYSTEM -> Markup.SYSTEM,
14.66 - Kind.STDIN -> Markup.STDIN,
14.67 - Kind.STDOUT -> Markup.STDOUT,
14.68 - Kind.SIGNAL -> Markup.SIGNAL,
14.69 - Kind.EXIT -> Markup.EXIT)
14.70 - //}}}
14.71 - def is_raw(kind: Value) =
14.72 - kind == STDOUT
14.73 - def is_control(kind: Value) =
14.74 - kind == SYSTEM ||
14.75 - kind == SIGNAL ||
14.76 - kind == EXIT
14.77 - def is_system(kind: Value) =
14.78 - kind == SYSTEM ||
14.79 - kind == STDIN ||
14.80 - kind == SIGNAL ||
14.81 - kind == EXIT ||
14.82 - kind == STATUS
14.83 - }
14.84 -
14.85 - class Result(val kind: Kind.Value, val props: List[(String, String)], val result: String) {
14.86 - override def toString = {
14.87 - val trees = YXML.parse_body_failsafe(result)
14.88 - val res =
14.89 - if (kind == Kind.STATUS) trees.map(_.toString).mkString
14.90 - else trees.flatMap(XML.content(_).mkString).mkString
14.91 - if (props.isEmpty)
14.92 - kind.toString + " [[" + res + "]]"
14.93 - else
14.94 - kind.toString + " " +
14.95 - (for ((x, y) <- props) yield x + "=" + y).mkString("{", ",", "}") + " [[" + res + "]]"
14.96 - }
14.97 - def is_raw = Kind.is_raw(kind)
14.98 - def is_control = Kind.is_control(kind)
14.99 - def is_system = Kind.is_system(kind)
14.100 - }
14.101 -
14.102 - def parse_message(isabelle_system: IsabelleSystem, result: Result) =
14.103 - {
14.104 - XML.Elem(Markup.MESSAGE, (Markup.CLASS, Kind.markup(result.kind)) :: result.props,
14.105 - YXML.parse_body_failsafe(isabelle_system.symbols.decode(result.result)))
14.106 - }
14.107 -}
14.108 -
14.109 -
14.110 -class IsabelleProcess(isabelle_system: IsabelleSystem,
14.111 - results: EventBus[IsabelleProcess.Result], args: String*)
14.112 -{
14.113 - import IsabelleProcess._
14.114 -
14.115 -
14.116 - /* demo constructor */
14.117 -
14.118 - def this(args: String*) =
14.119 - this(new IsabelleSystem, new EventBus[IsabelleProcess.Result] + Console.println, args: _*)
14.120 -
14.121 -
14.122 - /* process information */
14.123 -
14.124 - @volatile private var proc: Process = null
14.125 - @volatile private var closing = false
14.126 - @volatile private var pid: String = null
14.127 - @volatile private var the_session: String = null
14.128 - def session = the_session
14.129 -
14.130 -
14.131 - /* results */
14.132 -
14.133 - def parse_message(result: Result): XML.Tree =
14.134 - IsabelleProcess.parse_message(isabelle_system, result)
14.135 -
14.136 - private val result_queue = new LinkedBlockingQueue[Result]
14.137 -
14.138 - private def put_result(kind: Kind.Value, props: List[(String, String)], result: String)
14.139 - {
14.140 - if (kind == Kind.INIT) {
14.141 - val map = Map(props: _*)
14.142 - if (map.isDefinedAt(Markup.PID)) pid = map(Markup.PID)
14.143 - if (map.isDefinedAt(Markup.SESSION)) the_session = map(Markup.SESSION)
14.144 - }
14.145 - result_queue.put(new Result(kind, props, result))
14.146 - }
14.147 -
14.148 - private class ResultThread extends Thread("isabelle: results") {
14.149 - override def run() = {
14.150 - var finished = false
14.151 - while (!finished) {
14.152 - val result =
14.153 - try { result_queue.take }
14.154 - catch { case _: NullPointerException => null }
14.155 -
14.156 - if (result != null) {
14.157 - results.event(result)
14.158 - if (result.kind == Kind.EXIT) finished = true
14.159 - }
14.160 - else finished = true
14.161 - }
14.162 - }
14.163 - }
14.164 -
14.165 -
14.166 - /* signals */
14.167 -
14.168 - def interrupt() = synchronized {
14.169 - if (proc == null) error("Cannot interrupt Isabelle: no process")
14.170 - if (pid == null) put_result(Kind.SYSTEM, Nil, "Cannot interrupt: unknown pid")
14.171 - else {
14.172 - try {
14.173 - if (isabelle_system.execute(true, "kill", "-INT", pid).waitFor == 0)
14.174 - put_result(Kind.SIGNAL, Nil, "INT")
14.175 - else
14.176 - put_result(Kind.SYSTEM, Nil, "Cannot interrupt: kill command failed")
14.177 - }
14.178 - catch { case e: IOException => error("Cannot interrupt Isabelle: " + e.getMessage) }
14.179 - }
14.180 - }
14.181 -
14.182 - def kill() = synchronized {
14.183 - if (proc == 0) error("Cannot kill Isabelle: no process")
14.184 - else {
14.185 - try_close()
14.186 - Thread.sleep(500)
14.187 - put_result(Kind.SIGNAL, Nil, "KILL")
14.188 - proc.destroy
14.189 - proc = null
14.190 - pid = null
14.191 - }
14.192 - }
14.193 -
14.194 -
14.195 - /* output being piped into the process */
14.196 -
14.197 - private val output = new LinkedBlockingQueue[String]
14.198 -
14.199 - private def output_raw(text: String) = synchronized {
14.200 - if (proc == null) error("Cannot output to Isabelle: no process")
14.201 - if (closing) error("Cannot output to Isabelle: already closing")
14.202 - output.put(text)
14.203 - }
14.204 -
14.205 - def output_sync(text: String) =
14.206 - output_raw(" \\<^sync>\n; " + text + " \\<^sync>;\n")
14.207 -
14.208 -
14.209 - def command(text: String) =
14.210 - output_sync("Isabelle.command " + IsabelleSyntax.encode_string(text))
14.211 -
14.212 - def command(props: List[(String, String)], text: String) =
14.213 - output_sync("Isabelle.command " + IsabelleSyntax.encode_properties(props) + " " +
14.214 - IsabelleSyntax.encode_string(text))
14.215 -
14.216 - def ML(text: String) =
14.217 - output_sync("ML_val " + IsabelleSyntax.encode_string(text))
14.218 -
14.219 - def close() = synchronized { // FIXME watchdog/timeout
14.220 - output_raw("\u0000")
14.221 - closing = true
14.222 - }
14.223 -
14.224 - def try_close() = synchronized {
14.225 - if (proc != null && !closing) {
14.226 - try { close() }
14.227 - catch { case _: RuntimeException => }
14.228 - }
14.229 - }
14.230 -
14.231 -
14.232 - /* stdin */
14.233 -
14.234 - private class StdinThread(out_stream: OutputStream) extends Thread("isabelle: stdin") {
14.235 - override def run() = {
14.236 - val writer = new BufferedWriter(new OutputStreamWriter(out_stream, isabelle_system.charset))
14.237 - var finished = false
14.238 - while (!finished) {
14.239 - try {
14.240 - //{{{
14.241 - val s = output.take
14.242 - if (s == "\u0000") {
14.243 - writer.close
14.244 - finished = true
14.245 - }
14.246 - else {
14.247 - put_result(Kind.STDIN, Nil, s)
14.248 - writer.write(s)
14.249 - writer.flush
14.250 - }
14.251 - //}}}
14.252 - }
14.253 - catch {
14.254 - case e: IOException => put_result(Kind.SYSTEM, Nil, "Stdin thread: " + e.getMessage)
14.255 - }
14.256 - }
14.257 - put_result(Kind.SYSTEM, Nil, "Stdin thread terminated")
14.258 - }
14.259 - }
14.260 -
14.261 -
14.262 - /* stdout */
14.263 -
14.264 - private class StdoutThread(in_stream: InputStream) extends Thread("isabelle: stdout") {
14.265 - override def run() = {
14.266 - val reader = new BufferedReader(new InputStreamReader(in_stream, isabelle_system.charset))
14.267 - var result = new StringBuilder(100)
14.268 -
14.269 - var finished = false
14.270 - while (!finished) {
14.271 - try {
14.272 - //{{{
14.273 - var c = -1
14.274 - var done = false
14.275 - while (!done && (result.length == 0 || reader.ready)) {
14.276 - c = reader.read
14.277 - if (c >= 0) result.append(c.asInstanceOf[Char])
14.278 - else done = true
14.279 - }
14.280 - if (result.length > 0) {
14.281 - put_result(Kind.STDOUT, Nil, result.toString)
14.282 - result.length = 0
14.283 - }
14.284 - else {
14.285 - reader.close
14.286 - finished = true
14.287 - try_close()
14.288 - }
14.289 - //}}}
14.290 - }
14.291 - catch {
14.292 - case e: IOException => put_result(Kind.SYSTEM, Nil, "Stdout thread: " + e.getMessage)
14.293 - }
14.294 - }
14.295 - put_result(Kind.SYSTEM, Nil, "Stdout thread terminated")
14.296 - }
14.297 - }
14.298 -
14.299 -
14.300 - /* messages */
14.301 -
14.302 - private class MessageThread(fifo: String) extends Thread("isabelle: messages") {
14.303 - override def run() = {
14.304 - val reader = isabelle_system.fifo_reader(fifo)
14.305 - var kind: Kind.Value = null
14.306 - var props: List[(String, String)] = Nil
14.307 - var result = new StringBuilder
14.308 -
14.309 - var finished = false
14.310 - while (!finished) {
14.311 - try {
14.312 - if (kind == null) {
14.313 - //{{{ Char mode -- resync
14.314 - var c = -1
14.315 - do {
14.316 - c = reader.read
14.317 - if (c >= 0 && c != 2) result.append(c.asInstanceOf[Char])
14.318 - } while (c >= 0 && c != 2)
14.319 -
14.320 - if (result.length > 0) {
14.321 - put_result(Kind.SYSTEM, Nil, "Malformed message:\n" + result.toString)
14.322 - result.length = 0
14.323 - }
14.324 - if (c < 0) {
14.325 - reader.close
14.326 - finished = true
14.327 - try_close()
14.328 - }
14.329 - else {
14.330 - c = reader.read
14.331 - if (Kind.code.isDefinedAt(c)) kind = Kind.code(c)
14.332 - else kind = null
14.333 - }
14.334 - //}}}
14.335 - }
14.336 - else {
14.337 - //{{{ Line mode
14.338 - val line = reader.readLine
14.339 - if (line == null) {
14.340 - reader.close
14.341 - finished = true
14.342 - try_close()
14.343 - }
14.344 - else {
14.345 - val len = line.length
14.346 - // property
14.347 - if (line.endsWith("\u0002,")) {
14.348 - val i = line.indexOf('=')
14.349 - if (i > 0) {
14.350 - val name = line.substring(0, i)
14.351 - val value = line.substring(i + 1, len - 2)
14.352 - props = (name, value) :: props
14.353 - }
14.354 - }
14.355 - // last text line
14.356 - else if (line.endsWith("\u0002.")) {
14.357 - result.append(line.substring(0, len - 2))
14.358 - put_result(kind, props.reverse, result.toString)
14.359 - kind = null
14.360 - props = Nil
14.361 - result.length = 0
14.362 - }
14.363 - // text line
14.364 - else {
14.365 - result.append(line)
14.366 - result.append('\n')
14.367 - }
14.368 - }
14.369 - //}}}
14.370 - }
14.371 - }
14.372 - catch {
14.373 - case e: IOException => put_result(Kind.SYSTEM, Nil, "Message thread: " + e.getMessage)
14.374 - }
14.375 - }
14.376 - put_result(Kind.SYSTEM, Nil, "Message thread terminated")
14.377 - }
14.378 - }
14.379 -
14.380 -
14.381 -
14.382 - /** main **/
14.383 -
14.384 - {
14.385 - /* isabelle version */
14.386 -
14.387 - {
14.388 - val (msg, rc) = isabelle_system.isabelle_tool("version")
14.389 - if (rc != 0) error("Version check failed -- bad Isabelle installation:\n" + msg)
14.390 - put_result(Kind.SYSTEM, Nil, msg)
14.391 - }
14.392 -
14.393 -
14.394 - /* messages */
14.395 -
14.396 - val message_fifo = isabelle_system.mk_fifo()
14.397 - def rm_fifo() = isabelle_system.rm_fifo(message_fifo)
14.398 -
14.399 - val message_thread = new MessageThread(message_fifo)
14.400 - message_thread.start
14.401 -
14.402 - new ResultThread().start
14.403 -
14.404 -
14.405 - /* exec process */
14.406 -
14.407 - try {
14.408 - val cmdline =
14.409 - List(isabelle_system.getenv_strict("ISABELLE_PROCESS"), "-W", message_fifo) ++ args
14.410 - proc = isabelle_system.execute(true, cmdline: _*)
14.411 - }
14.412 - catch {
14.413 - case e: IOException =>
14.414 - rm_fifo()
14.415 - error("Failed to execute Isabelle process: " + e.getMessage)
14.416 - }
14.417 -
14.418 -
14.419 - /* stdin/stdout */
14.420 -
14.421 - new StdinThread(proc.getOutputStream).start
14.422 - new StdoutThread(proc.getInputStream).start
14.423 -
14.424 -
14.425 - /* exit */
14.426 -
14.427 - new Thread("isabelle: exit") {
14.428 - override def run() = {
14.429 - val rc = proc.waitFor()
14.430 - Thread.sleep(300)
14.431 - put_result(Kind.SYSTEM, Nil, "Exit thread terminated")
14.432 - put_result(Kind.EXIT, Nil, Integer.toString(rc))
14.433 - rm_fifo()
14.434 - }
14.435 - }.start
14.436 -
14.437 - }
14.438 -}