# HG changeset patch # User wenzelm # Date 1251881692 -7200 # Node ID 1521d879daf4ab909c51d2d68720d60e6856f655 # Parent 6009d48bba096061f726f6939858079725bc3423# Parent 4af24f127fcf9ed7500531bd46aa77ed1896fb09 merged diff -r 6009d48bba09 -r 1521d879daf4 src/Pure/IsaMakefile --- a/src/Pure/IsaMakefile Tue Sep 01 21:46:38 2009 +0200 +++ b/src/Pure/IsaMakefile Wed Sep 02 10:54:52 2009 +0200 @@ -120,8 +120,8 @@ SCALA_FILES = General/event_bus.scala General/linear_set.scala \ General/markup.scala General/position.scala General/scan.scala \ General/swing_thread.scala General/symbol.scala General/xml.scala \ - General/yxml.scala Isar/isar.scala Isar/isar_document.scala \ - Isar/outer_keyword.scala System/cygwin.scala System/gui_setup.scala \ + General/yxml.scala Isar/isar_document.scala Isar/outer_keyword.scala \ + System/cygwin.scala System/gui_setup.scala \ System/isabelle_process.scala System/isabelle_syntax.scala \ System/isabelle_system.scala System/platform.scala \ Thy/completion.scala Thy/thy_header.scala diff -r 6009d48bba09 -r 1521d879daf4 src/Pure/Isar/isar.scala --- a/src/Pure/Isar/isar.scala Tue Sep 01 21:46:38 2009 +0200 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,26 +0,0 @@ -/* Title: Pure/Isar/isar.scala - Author: Makarius - -Isar document model. -*/ - -package isabelle - - -class Isar(isabelle_system: Isabelle_System, - results: EventBus[Isabelle_Process.Result], args: String*) - extends Isabelle_Process(isabelle_system, results, args: _*) -{ - /* basic editor commands */ - - def create_command(id: String, text: String) = - output_sync("Isar.command " + Isabelle_Syntax.encode_string(id) + " " + - Isabelle_Syntax.encode_string(text)) - - def insert_command(prev: String, id: String) = - output_sync("Isar.insert " + Isabelle_Syntax.encode_string(prev) + " " + - Isabelle_Syntax.encode_string(id)) - - def remove_command(id: String) = - output_sync("Isar.remove " + Isabelle_Syntax.encode_string(id)) -} diff -r 6009d48bba09 -r 1521d879daf4 src/Pure/System/isabelle_process.scala --- a/src/Pure/System/isabelle_process.scala Tue Sep 01 21:46:38 2009 +0200 +++ b/src/Pure/System/isabelle_process.scala Wed Sep 02 10:54:52 2009 +0200 @@ -11,9 +11,12 @@ import java.io.{BufferedReader, BufferedWriter, InputStreamReader, OutputStreamWriter, InputStream, OutputStream, IOException} +import scala.actors.Actor +import Actor._ -object Isabelle_Process { +object Isabelle_Process +{ /* results */ object Kind extends Enumeration { @@ -104,8 +107,7 @@ } -class Isabelle_Process(isabelle_system: Isabelle_System, - results: EventBus[Isabelle_Process.Result], args: String*) +class Isabelle_Process(isabelle_system: Isabelle_System, receiver: Actor, args: String*) { import Isabelle_Process._ @@ -113,7 +115,8 @@ /* demo constructor */ def this(args: String*) = - this(new Isabelle_System, new EventBus[Isabelle_Process.Result] + Console.println, args: _*) + this(new Isabelle_System, + new Actor { def act = loop { react { case res => Console.println(res) } } }.start, args: _*) /* process information */ @@ -127,11 +130,6 @@ /* results */ - def parse_message(result: Result): XML.Tree = - Isabelle_Process.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) { @@ -139,24 +137,7 @@ 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 - } - } + receiver ! new Result(kind, props, result) } @@ -396,8 +377,6 @@ val message_thread = new MessageThread(message_fifo) message_thread.start - new ResultThread().start - /* exec process */ diff -r 6009d48bba09 -r 1521d879daf4 src/Pure/System/isar.ML --- a/src/Pure/System/isar.ML Tue Sep 01 21:46:38 2009 +0200 +++ b/src/Pure/System/isar.ML Wed Sep 02 10:54:52 2009 +0200 @@ -22,12 +22,6 @@ 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 = @@ -145,7 +139,7 @@ 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 do_init then init () else (); if welcome then writeln (Session.welcome ()) else (); uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ()); @@ -159,198 +153,6 @@ -(** 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 "i" ^ 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 @@ -392,24 +194,6 @@ 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;