removed old Isar document model;
authorwenzelm
Tue Sep 01 21:40:10 2009 +0200 (2009-09-01)
changeset 3248667972a7f85b7
parent 32474 0818e6b1c8a6
child 32487 4af24f127fcf
removed old Isar document model;
src/Pure/IsaMakefile
src/Pure/Isar/isar.scala
src/Pure/System/isar.ML
     1.1 --- a/src/Pure/IsaMakefile	Tue Sep 01 21:03:04 2009 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Tue Sep 01 21:40:10 2009 +0200
     1.3 @@ -120,8 +120,8 @@
     1.4  SCALA_FILES = General/event_bus.scala General/linear_set.scala		\
     1.5    General/markup.scala General/position.scala General/scan.scala	\
     1.6    General/swing_thread.scala General/symbol.scala General/xml.scala	\
     1.7 -  General/yxml.scala Isar/isar.scala Isar/isar_document.scala		\
     1.8 -  Isar/outer_keyword.scala System/cygwin.scala System/gui_setup.scala	\
     1.9 +  General/yxml.scala Isar/isar_document.scala Isar/outer_keyword.scala	\
    1.10 +  System/cygwin.scala System/gui_setup.scala				\
    1.11    System/isabelle_process.scala System/isabelle_syntax.scala		\
    1.12    System/isabelle_system.scala System/platform.scala			\
    1.13    Thy/completion.scala Thy/thy_header.scala
     2.1 --- a/src/Pure/Isar/isar.scala	Tue Sep 01 21:03:04 2009 +0200
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,27 +0,0 @@
     2.4 -/*  Title:      Pure/Isar/isar.scala
     2.5 -    Author:     Makarius
     2.6 -
     2.7 -Isar document model.
     2.8 -*/
     2.9 -
    2.10 -package isabelle
    2.11 -
    2.12 -import scala.actors.Actor
    2.13 -
    2.14 -
    2.15 -class Isar(isabelle_system: Isabelle_System, receiver: Actor, args: String*)
    2.16 -  extends Isabelle_Process(isabelle_system, receiver, args: _*)
    2.17 -{
    2.18 -  /* basic editor commands */
    2.19 -
    2.20 -  def create_command(id: String, text: String) =
    2.21 -    output_sync("Isar.command " + Isabelle_Syntax.encode_string(id) + " " +
    2.22 -      Isabelle_Syntax.encode_string(text))
    2.23 -
    2.24 -  def insert_command(prev: String, id: String) =
    2.25 -    output_sync("Isar.insert " + Isabelle_Syntax.encode_string(prev) + " " +
    2.26 -      Isabelle_Syntax.encode_string(id))
    2.27 -
    2.28 -  def remove_command(id: String) =
    2.29 -    output_sync("Isar.remove " + Isabelle_Syntax.encode_string(id))
    2.30 -}
     3.1 --- a/src/Pure/System/isar.ML	Tue Sep 01 21:03:04 2009 +0200
     3.2 +++ b/src/Pure/System/isar.ML	Tue Sep 01 21:40:10 2009 +0200
     3.3 @@ -22,12 +22,6 @@
     3.4    val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
     3.5    val loop: unit -> unit
     3.6    val main: unit -> unit
     3.7 -
     3.8 -  type id = string
     3.9 -  val no_id: id
    3.10 -  val create_command: Toplevel.transition -> id
    3.11 -  val insert_command: id -> id -> unit
    3.12 -  val remove_command: id -> unit
    3.13  end;
    3.14  
    3.15  structure Isar: ISAR =
    3.16 @@ -145,7 +139,7 @@
    3.17  
    3.18  fun toplevel_loop {init = do_init, welcome, sync, secure} =
    3.19   (Context.set_thread_data NONE;
    3.20 -  if do_init then init () else ();  (* FIXME init editor model *)
    3.21 +  if do_init then init () else ();
    3.22    if welcome then writeln (Session.welcome ()) else ();
    3.23    uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ());
    3.24  
    3.25 @@ -159,198 +153,6 @@
    3.26  
    3.27  
    3.28  
    3.29 -(** individual toplevel commands **)
    3.30 -
    3.31 -(* unique identification *)
    3.32 -
    3.33 -type id = string;
    3.34 -val no_id : id = "";
    3.35 -
    3.36 -
    3.37 -(* command category *)
    3.38 -
    3.39 -datatype category = Empty | Theory | Proof | Diag | Control;
    3.40 -
    3.41 -fun category_of tr =
    3.42 -  let val name = Toplevel.name_of tr in
    3.43 -    if name = "" then Empty
    3.44 -    else if OuterKeyword.is_theory name then Theory
    3.45 -    else if OuterKeyword.is_proof name then Proof
    3.46 -    else if OuterKeyword.is_diag name then Diag
    3.47 -    else Control
    3.48 -  end;
    3.49 -
    3.50 -val is_theory = fn Theory => true | _ => false;
    3.51 -val is_proper = fn Theory => true | Proof => true | _ => false;
    3.52 -val is_regular = fn Control => false | _ => true;
    3.53 -
    3.54 -
    3.55 -(* command status *)
    3.56 -
    3.57 -datatype status =
    3.58 -  Unprocessed |
    3.59 -  Running |
    3.60 -  Failed of exn * string |
    3.61 -  Finished of Toplevel.state;
    3.62 -
    3.63 -fun status_markup Unprocessed = Markup.unprocessed
    3.64 -  | status_markup Running = (Markup.runningN, [])
    3.65 -  | status_markup (Failed _) = Markup.failed
    3.66 -  | status_markup (Finished _) = Markup.finished;
    3.67 -
    3.68 -fun run int tr state =
    3.69 -  (case Toplevel.transition int tr state of
    3.70 -    NONE => NONE
    3.71 -  | SOME (_, SOME err) => (Toplevel.error_msg tr err; SOME (Failed err))
    3.72 -  | SOME (state', NONE) => SOME (Finished state'));
    3.73 -
    3.74 -
    3.75 -(* datatype command *)
    3.76 -
    3.77 -datatype command = Command of
    3.78 - {category: category,
    3.79 -  transition: Toplevel.transition,
    3.80 -  status: status};
    3.81 -
    3.82 -fun make_command (category, transition, status) =
    3.83 -  Command {category = category, transition = transition, status = status};
    3.84 -
    3.85 -val empty_command =
    3.86 -  make_command (Empty, Toplevel.empty, Finished Toplevel.toplevel);
    3.87 -
    3.88 -fun map_command f (Command {category, transition, status}) =
    3.89 -  make_command (f (category, transition, status));
    3.90 -
    3.91 -fun map_status f = map_command (fn (category, transition, status) =>
    3.92 -  (category, transition, f status));
    3.93 -
    3.94 -
    3.95 -(* global collection of identified commands *)
    3.96 -
    3.97 -fun err_dup id = sys_error ("Duplicate command " ^ quote id);
    3.98 -fun err_undef id = sys_error ("Unknown command " ^ quote id);
    3.99 -
   3.100 -local val global_commands = ref (Graph.empty: command Graph.T) in
   3.101 -
   3.102 -fun change_commands f = NAMED_CRITICAL "Isar" (fn () => change global_commands f)
   3.103 -  handle Graph.DUP bad => err_dup bad | Graph.UNDEF bad => err_undef bad;
   3.104 -
   3.105 -fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands);
   3.106 -
   3.107 -end;
   3.108 -
   3.109 -fun add_edge (id1, id2) =
   3.110 -  if id1 = no_id orelse id2 = no_id then I else Graph.add_edge (id1, id2);
   3.111 -
   3.112 -
   3.113 -fun init_commands () = change_commands (K Graph.empty);
   3.114 -
   3.115 -fun the_command id =
   3.116 -  let val Command cmd =
   3.117 -    if id = no_id then empty_command
   3.118 -    else (Graph.get_node (get_commands ()) id handle Graph.UNDEF bad => err_undef bad)
   3.119 -  in cmd end;
   3.120 -
   3.121 -fun prev_command id =
   3.122 -  if id = no_id then no_id
   3.123 -  else
   3.124 -    (case Graph.imm_preds (get_commands ()) id handle Graph.UNDEF bad => err_undef bad of
   3.125 -      [] => no_id
   3.126 -    | [prev] => prev
   3.127 -    | _ => sys_error ("Non-linear command dependency " ^ quote id));
   3.128 -
   3.129 -fun next_commands id =
   3.130 -  if id = no_id then []
   3.131 -  else Graph.imm_succs (get_commands ()) id handle Graph.UNDEF bad => err_undef bad;
   3.132 -
   3.133 -fun descendant_commands ids =
   3.134 -  Graph.all_succs (get_commands ()) (distinct (op =) (filter_out (fn id => id = no_id) ids))
   3.135 -    handle Graph.UNDEF bad => err_undef bad;
   3.136 -
   3.137 -
   3.138 -(* maintain status *)
   3.139 -
   3.140 -fun report_status markup id = Toplevel.status (#transition (the_command id)) markup;
   3.141 -
   3.142 -fun update_status status id = change_commands (Graph.map_node id (map_status (K status)));
   3.143 -
   3.144 -fun report_update_status status id =
   3.145 -  change_commands (Graph.map_node id (map_status (fn old_status =>
   3.146 -    let val markup = status_markup status
   3.147 -    in if markup <> status_markup old_status then report_status markup id else (); status end)));
   3.148 -
   3.149 -
   3.150 -(* create and dispose commands *)
   3.151 -
   3.152 -fun create_command raw_tr =
   3.153 -  let
   3.154 -    val (id, tr) =
   3.155 -      (case Toplevel.get_id raw_tr of
   3.156 -        SOME id => (id, raw_tr)
   3.157 -      | NONE =>
   3.158 -          let val id =
   3.159 -            if ! Toplevel.debug then "isabelle:" ^ Toplevel.name_of raw_tr ^ serial_string ()
   3.160 -            else "i" ^ serial_string ()
   3.161 -          in (id, Toplevel.put_id id raw_tr) end);
   3.162 -
   3.163 -    val cmd = make_command (category_of tr, tr, Unprocessed);
   3.164 -    val _ = change_commands (Graph.new_node (id, cmd));
   3.165 -  in id end;
   3.166 -
   3.167 -fun dispose_commands ids =
   3.168 -  let
   3.169 -    val desc = descendant_commands ids;
   3.170 -    val _ = List.app (report_status Markup.disposed) desc;
   3.171 -    val _ = change_commands (Graph.del_nodes desc);
   3.172 -  in () end;
   3.173 -
   3.174 -
   3.175 -(* final state *)
   3.176 -
   3.177 -fun the_state id =
   3.178 -  (case the_command id of
   3.179 -    {status = Finished state, ...} => state
   3.180 -  | {transition, ...} => error ("Unfinished command " ^ Toplevel.str_of transition));
   3.181 -
   3.182 -
   3.183 -
   3.184 -(** editor model **)
   3.185 -
   3.186 -(* run commands *)
   3.187 -
   3.188 -fun try_run id =
   3.189 -  (case try the_state (prev_command id) of
   3.190 -    NONE => ()
   3.191 -  | SOME state =>
   3.192 -      (case run true (#transition (the_command id)) state of
   3.193 -        NONE => ()
   3.194 -      | SOME status => report_update_status status id));
   3.195 -
   3.196 -fun rerun_commands ids =
   3.197 -  (List.app (report_update_status Unprocessed) ids; List.app try_run ids);
   3.198 -
   3.199 -
   3.200 -(* modify document *)
   3.201 -
   3.202 -fun insert_command prev id = NAMED_CRITICAL "Isar" (fn () =>
   3.203 -  let
   3.204 -    val nexts = next_commands prev;
   3.205 -    val _ = change_commands
   3.206 -     (fold (fn next => Graph.del_edge (prev, next)) nexts #> add_edge (prev, id) #>
   3.207 -      fold (fn next => Graph.add_edge (id, next)) nexts);
   3.208 -  in descendant_commands [id] end) |> rerun_commands;
   3.209 -
   3.210 -fun remove_command id = NAMED_CRITICAL "Isar" (fn () =>
   3.211 -  let
   3.212 -    val prev = prev_command id;
   3.213 -    val nexts = next_commands id;
   3.214 -    val _ = change_commands
   3.215 -     (fold (fn next => Graph.del_edge (id, next)) nexts #>
   3.216 -      fold (fn next => add_edge (prev, next)) nexts);
   3.217 -  in descendant_commands nexts end) |> rerun_commands;
   3.218 -
   3.219 -
   3.220 -
   3.221  (** command syntax **)
   3.222  
   3.223  local
   3.224 @@ -392,24 +194,6 @@
   3.225    OuterSyntax.improper_command "kill" "kill partial proof or theory development" K.control
   3.226      (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
   3.227  
   3.228 -
   3.229 -(* editor model *)
   3.230 -
   3.231 -val _ =
   3.232 -  OuterSyntax.internal_command "Isar.command"
   3.233 -    (P.string -- P.string >> (fn (id, text) =>
   3.234 -      Toplevel.imperative (fn () =>
   3.235 -        ignore (create_command (OuterSyntax.prepare_command (Position.id id) text)))));
   3.236 -
   3.237 -val _ =
   3.238 -  OuterSyntax.internal_command "Isar.insert"
   3.239 -    (P.string -- P.string >> (fn (prev, id) =>
   3.240 -      Toplevel.imperative (fn () => insert_command prev id)));
   3.241 -
   3.242 -val _ =
   3.243 -  OuterSyntax.internal_command "Isar.remove"
   3.244 -    (P.string >> (fn id => Toplevel.imperative (fn () => remove_command id)));
   3.245 -
   3.246  end;
   3.247  
   3.248  end;