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