src/Pure/System/isar.ML
changeset 32486 67972a7f85b7
parent 31478 5e412e4c6546
child 32738 15bb09ca0378
     1.1 --- a/src/Pure/System/isar.ML	Tue Sep 01 21:03:04 2009 +0200
     1.2 +++ b/src/Pure/System/isar.ML	Tue Sep 01 21:40:10 2009 +0200
     1.3 @@ -22,12 +22,6 @@
     1.4    val toplevel_loop: {init: bool, welcome: bool, sync: bool, secure: bool} -> unit
     1.5    val loop: unit -> unit
     1.6    val main: unit -> unit
     1.7 -
     1.8 -  type id = string
     1.9 -  val no_id: id
    1.10 -  val create_command: Toplevel.transition -> id
    1.11 -  val insert_command: id -> id -> unit
    1.12 -  val remove_command: id -> unit
    1.13  end;
    1.14  
    1.15  structure Isar: ISAR =
    1.16 @@ -145,7 +139,7 @@
    1.17  
    1.18  fun toplevel_loop {init = do_init, welcome, sync, secure} =
    1.19   (Context.set_thread_data NONE;
    1.20 -  if do_init then init () else ();  (* FIXME init editor model *)
    1.21 +  if do_init then init () else ();
    1.22    if welcome then writeln (Session.welcome ()) else ();
    1.23    uninterruptible (fn _ => fn () => raw_loop secure (OuterSyntax.isar sync)) ());
    1.24  
    1.25 @@ -159,198 +153,6 @@
    1.26  
    1.27  
    1.28  
    1.29 -(** individual toplevel commands **)
    1.30 -
    1.31 -(* unique identification *)
    1.32 -
    1.33 -type id = string;
    1.34 -val no_id : id = "";
    1.35 -
    1.36 -
    1.37 -(* command category *)
    1.38 -
    1.39 -datatype category = Empty | Theory | Proof | Diag | Control;
    1.40 -
    1.41 -fun category_of tr =
    1.42 -  let val name = Toplevel.name_of tr in
    1.43 -    if name = "" then Empty
    1.44 -    else if OuterKeyword.is_theory name then Theory
    1.45 -    else if OuterKeyword.is_proof name then Proof
    1.46 -    else if OuterKeyword.is_diag name then Diag
    1.47 -    else Control
    1.48 -  end;
    1.49 -
    1.50 -val is_theory = fn Theory => true | _ => false;
    1.51 -val is_proper = fn Theory => true | Proof => true | _ => false;
    1.52 -val is_regular = fn Control => false | _ => true;
    1.53 -
    1.54 -
    1.55 -(* command status *)
    1.56 -
    1.57 -datatype status =
    1.58 -  Unprocessed |
    1.59 -  Running |
    1.60 -  Failed of exn * string |
    1.61 -  Finished of Toplevel.state;
    1.62 -
    1.63 -fun status_markup Unprocessed = Markup.unprocessed
    1.64 -  | status_markup Running = (Markup.runningN, [])
    1.65 -  | status_markup (Failed _) = Markup.failed
    1.66 -  | status_markup (Finished _) = Markup.finished;
    1.67 -
    1.68 -fun run int tr state =
    1.69 -  (case Toplevel.transition int tr state of
    1.70 -    NONE => NONE
    1.71 -  | SOME (_, SOME err) => (Toplevel.error_msg tr err; SOME (Failed err))
    1.72 -  | SOME (state', NONE) => SOME (Finished state'));
    1.73 -
    1.74 -
    1.75 -(* datatype command *)
    1.76 -
    1.77 -datatype command = Command of
    1.78 - {category: category,
    1.79 -  transition: Toplevel.transition,
    1.80 -  status: status};
    1.81 -
    1.82 -fun make_command (category, transition, status) =
    1.83 -  Command {category = category, transition = transition, status = status};
    1.84 -
    1.85 -val empty_command =
    1.86 -  make_command (Empty, Toplevel.empty, Finished Toplevel.toplevel);
    1.87 -
    1.88 -fun map_command f (Command {category, transition, status}) =
    1.89 -  make_command (f (category, transition, status));
    1.90 -
    1.91 -fun map_status f = map_command (fn (category, transition, status) =>
    1.92 -  (category, transition, f status));
    1.93 -
    1.94 -
    1.95 -(* global collection of identified commands *)
    1.96 -
    1.97 -fun err_dup id = sys_error ("Duplicate command " ^ quote id);
    1.98 -fun err_undef id = sys_error ("Unknown command " ^ quote id);
    1.99 -
   1.100 -local val global_commands = ref (Graph.empty: command Graph.T) in
   1.101 -
   1.102 -fun change_commands f = NAMED_CRITICAL "Isar" (fn () => change global_commands f)
   1.103 -  handle Graph.DUP bad => err_dup bad | Graph.UNDEF bad => err_undef bad;
   1.104 -
   1.105 -fun get_commands () = NAMED_CRITICAL "Isar" (fn () => ! global_commands);
   1.106 -
   1.107 -end;
   1.108 -
   1.109 -fun add_edge (id1, id2) =
   1.110 -  if id1 = no_id orelse id2 = no_id then I else Graph.add_edge (id1, id2);
   1.111 -
   1.112 -
   1.113 -fun init_commands () = change_commands (K Graph.empty);
   1.114 -
   1.115 -fun the_command id =
   1.116 -  let val Command cmd =
   1.117 -    if id = no_id then empty_command
   1.118 -    else (Graph.get_node (get_commands ()) id handle Graph.UNDEF bad => err_undef bad)
   1.119 -  in cmd end;
   1.120 -
   1.121 -fun prev_command id =
   1.122 -  if id = no_id then no_id
   1.123 -  else
   1.124 -    (case Graph.imm_preds (get_commands ()) id handle Graph.UNDEF bad => err_undef bad of
   1.125 -      [] => no_id
   1.126 -    | [prev] => prev
   1.127 -    | _ => sys_error ("Non-linear command dependency " ^ quote id));
   1.128 -
   1.129 -fun next_commands id =
   1.130 -  if id = no_id then []
   1.131 -  else Graph.imm_succs (get_commands ()) id handle Graph.UNDEF bad => err_undef bad;
   1.132 -
   1.133 -fun descendant_commands ids =
   1.134 -  Graph.all_succs (get_commands ()) (distinct (op =) (filter_out (fn id => id = no_id) ids))
   1.135 -    handle Graph.UNDEF bad => err_undef bad;
   1.136 -
   1.137 -
   1.138 -(* maintain status *)
   1.139 -
   1.140 -fun report_status markup id = Toplevel.status (#transition (the_command id)) markup;
   1.141 -
   1.142 -fun update_status status id = change_commands (Graph.map_node id (map_status (K status)));
   1.143 -
   1.144 -fun report_update_status status id =
   1.145 -  change_commands (Graph.map_node id (map_status (fn old_status =>
   1.146 -    let val markup = status_markup status
   1.147 -    in if markup <> status_markup old_status then report_status markup id else (); status end)));
   1.148 -
   1.149 -
   1.150 -(* create and dispose commands *)
   1.151 -
   1.152 -fun create_command raw_tr =
   1.153 -  let
   1.154 -    val (id, tr) =
   1.155 -      (case Toplevel.get_id raw_tr of
   1.156 -        SOME id => (id, raw_tr)
   1.157 -      | NONE =>
   1.158 -          let val id =
   1.159 -            if ! Toplevel.debug then "isabelle:" ^ Toplevel.name_of raw_tr ^ serial_string ()
   1.160 -            else "i" ^ serial_string ()
   1.161 -          in (id, Toplevel.put_id id raw_tr) end);
   1.162 -
   1.163 -    val cmd = make_command (category_of tr, tr, Unprocessed);
   1.164 -    val _ = change_commands (Graph.new_node (id, cmd));
   1.165 -  in id end;
   1.166 -
   1.167 -fun dispose_commands ids =
   1.168 -  let
   1.169 -    val desc = descendant_commands ids;
   1.170 -    val _ = List.app (report_status Markup.disposed) desc;
   1.171 -    val _ = change_commands (Graph.del_nodes desc);
   1.172 -  in () end;
   1.173 -
   1.174 -
   1.175 -(* final state *)
   1.176 -
   1.177 -fun the_state id =
   1.178 -  (case the_command id of
   1.179 -    {status = Finished state, ...} => state
   1.180 -  | {transition, ...} => error ("Unfinished command " ^ Toplevel.str_of transition));
   1.181 -
   1.182 -
   1.183 -
   1.184 -(** editor model **)
   1.185 -
   1.186 -(* run commands *)
   1.187 -
   1.188 -fun try_run id =
   1.189 -  (case try the_state (prev_command id) of
   1.190 -    NONE => ()
   1.191 -  | SOME state =>
   1.192 -      (case run true (#transition (the_command id)) state of
   1.193 -        NONE => ()
   1.194 -      | SOME status => report_update_status status id));
   1.195 -
   1.196 -fun rerun_commands ids =
   1.197 -  (List.app (report_update_status Unprocessed) ids; List.app try_run ids);
   1.198 -
   1.199 -
   1.200 -(* modify document *)
   1.201 -
   1.202 -fun insert_command prev id = NAMED_CRITICAL "Isar" (fn () =>
   1.203 -  let
   1.204 -    val nexts = next_commands prev;
   1.205 -    val _ = change_commands
   1.206 -     (fold (fn next => Graph.del_edge (prev, next)) nexts #> add_edge (prev, id) #>
   1.207 -      fold (fn next => Graph.add_edge (id, next)) nexts);
   1.208 -  in descendant_commands [id] end) |> rerun_commands;
   1.209 -
   1.210 -fun remove_command id = NAMED_CRITICAL "Isar" (fn () =>
   1.211 -  let
   1.212 -    val prev = prev_command id;
   1.213 -    val nexts = next_commands id;
   1.214 -    val _ = change_commands
   1.215 -     (fold (fn next => Graph.del_edge (id, next)) nexts #>
   1.216 -      fold (fn next => add_edge (prev, next)) nexts);
   1.217 -  in descendant_commands nexts end) |> rerun_commands;
   1.218 -
   1.219 -
   1.220 -
   1.221  (** command syntax **)
   1.222  
   1.223  local
   1.224 @@ -392,24 +194,6 @@
   1.225    OuterSyntax.improper_command "kill" "kill partial proof or theory development" K.control
   1.226      (Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
   1.227  
   1.228 -
   1.229 -(* editor model *)
   1.230 -
   1.231 -val _ =
   1.232 -  OuterSyntax.internal_command "Isar.command"
   1.233 -    (P.string -- P.string >> (fn (id, text) =>
   1.234 -      Toplevel.imperative (fn () =>
   1.235 -        ignore (create_command (OuterSyntax.prepare_command (Position.id id) text)))));
   1.236 -
   1.237 -val _ =
   1.238 -  OuterSyntax.internal_command "Isar.insert"
   1.239 -    (P.string -- P.string >> (fn (prev, id) =>
   1.240 -      Toplevel.imperative (fn () => insert_command prev id)));
   1.241 -
   1.242 -val _ =
   1.243 -  OuterSyntax.internal_command "Isar.remove"
   1.244 -    (P.string >> (fn id => Toplevel.imperative (fn () => remove_command id)));
   1.245 -
   1.246  end;
   1.247  
   1.248  end;