--- a/src/Pure/IsaMakefile Tue Sep 01 21:03:04 2009 +0200
+++ b/src/Pure/IsaMakefile Tue Sep 01 21:40:10 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
--- a/src/Pure/Isar/isar.scala Tue Sep 01 21:03:04 2009 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,27 +0,0 @@
-/* Title: Pure/Isar/isar.scala
- Author: Makarius
-
-Isar document model.
-*/
-
-package isabelle
-
-import scala.actors.Actor
-
-
-class Isar(isabelle_system: Isabelle_System, receiver: Actor, args: String*)
- extends Isabelle_Process(isabelle_system, receiver, 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))
-}
--- a/src/Pure/System/isar.ML Tue Sep 01 21:03:04 2009 +0200
+++ b/src/Pure/System/isar.ML Tue Sep 01 21:40:10 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;