moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
authorwenzelm
Sat Feb 28 18:00:20 2009 +0100 (2009-02-28)
changeset 30173eabece26b89b
parent 30172 afdf7808cfd0
child 30174 7291e03cdb44
moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands);
src/Pure/IsaMakefile
src/Pure/Isar/ROOT.ML
src/Pure/Isar/isar.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/session.ML
src/Pure/ROOT.ML
src/Pure/System/isabelle_process.ML
src/Pure/System/isabelle_process.scala
src/Pure/System/isar.ML
src/Pure/System/session.ML
src/Pure/Tools/ROOT.ML
src/Pure/Tools/isabelle_process.ML
src/Pure/Tools/isabelle_process.scala
     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 -}