src/Pure/PIDE/document.ML
author wenzelm
Mon Jul 11 22:55:47 2011 +0200 (2011-07-11)
changeset 43761 e72ba84ae58f
parent 43722 9b5dadb0c28d
child 44113 0baa8bbd355a
permissions -rw-r--r--
tuned signature -- corresponding to Scala version;
     1 (*  Title:      Pure/PIDE/document.ML
     2     Author:     Makarius
     3 
     4 Document as collection of named nodes, each consisting of an editable
     5 list of commands, associated with asynchronous execution process.
     6 *)
     7 
     8 signature DOCUMENT =
     9 sig
    10   type id = int
    11   type version_id = id
    12   type command_id = id
    13   type exec_id = id
    14   val no_id: id
    15   val new_id: unit -> id
    16   val parse_id: string -> id
    17   val print_id: id -> string
    18   type edit = string * ((command_id option * command_id option) list) option
    19   type header = string * (string * string list * string list)
    20   type state
    21   val init_state: state
    22   val get_theory: state -> version_id -> Position.T -> string -> theory
    23   val cancel_execution: state -> unit -> unit
    24   val define_command: command_id -> string -> state -> state
    25   val edit: version_id -> version_id -> edit list -> header list ->
    26     state -> (command_id * exec_id) list * state
    27   val execute: version_id -> state -> state
    28   val state: unit -> state
    29   val change_state: (state -> state) -> unit
    30 end;
    31 
    32 structure Document: DOCUMENT =
    33 struct
    34 
    35 (* unique identifiers *)
    36 
    37 type id = int;
    38 type version_id = id;
    39 type command_id = id;
    40 type exec_id = id;
    41 
    42 val no_id = 0;
    43 val new_id = Synchronized.counter ();
    44 
    45 val parse_id = Markup.parse_int;
    46 val print_id = Markup.print_int;
    47 
    48 fun err_dup kind id = error ("Duplicate " ^ kind ^ ": " ^ print_id id);
    49 fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ print_id id);
    50 
    51 
    52 
    53 (** document structure **)
    54 
    55 structure Entries = Linear_Set(type key = command_id val ord = int_ord);
    56 
    57 abstype node = Node of
    58   {last: exec_id, entries: exec_id option Entries.T}  (*command entries with excecutions*)
    59 and version = Version of node Graph.T  (*development graph wrt. static imports*)
    60 with
    61 
    62 fun make_node (last, entries) =
    63   Node {last = last, entries = entries};
    64 
    65 fun get_last (Node {last, ...}) = last;
    66 fun set_last last (Node {entries, ...}) = make_node (last, entries);
    67 
    68 fun map_entries f (Node {last, entries}) = make_node (last, f entries);
    69 fun fold_entries start f (Node {entries, ...}) = Entries.fold start f entries;
    70 fun first_entry start P (Node {entries, ...}) = Entries.get_first start P entries;
    71 
    72 val empty_node = make_node (no_id, Entries.empty);
    73 val empty_version = Version Graph.empty;
    74 
    75 
    76 (* node edits and associated executions *)
    77 
    78 type edit =
    79   string *
    80   (*NONE: remove node, SOME: insert/remove commands*)
    81   ((command_id option * command_id option) list) option;
    82 
    83 type header = string * (string * string list * string list);
    84 
    85 fun the_entry (Node {entries, ...}) id =
    86   (case Entries.lookup entries id of
    87     NONE => err_undef "command entry" id
    88   | SOME entry => entry);
    89 
    90 fun update_entry (id, exec_id) =
    91   map_entries (Entries.update (id, SOME exec_id));
    92 
    93 fun reset_after id entries =
    94   (case Entries.get_after entries id of
    95     NONE => entries
    96   | SOME next => Entries.update (next, NONE) entries);
    97 
    98 val edit_node = map_entries o fold
    99   (fn (id, SOME id2) => Entries.insert_after id (id2, NONE)
   100     | (id, NONE) => Entries.delete_after id #> reset_after id);
   101 
   102 
   103 (* version operations *)
   104 
   105 fun nodes_of (Version nodes) = nodes;
   106 val node_names_of = Graph.keys o nodes_of;
   107 
   108 fun get_node version name = Graph.get_node (nodes_of version) name
   109   handle Graph.UNDEF _ => empty_node;
   110 
   111 fun edit_nodes (name, SOME edits) (Version nodes) =
   112       Version (nodes
   113         |> Graph.default_node (name, empty_node)
   114         |> Graph.map_node name (edit_node edits))
   115   | edit_nodes (name, NONE) (Version nodes) =
   116       Version (perhaps (try (Graph.del_node name)) nodes);
   117 
   118 fun put_node name node (Version nodes) =
   119   Version (nodes
   120     |> Graph.default_node (name, empty_node)
   121     |> Graph.map_node name (K node));
   122 
   123 end;
   124 
   125 
   126 
   127 (** global state -- document structure and execution process **)
   128 
   129 abstype state = State of
   130  {versions: version Inttab.table,  (*version_id -> document content*)
   131   commands: Toplevel.transition future Inttab.table,  (*command_id -> transition (future parsing)*)
   132   execs: (bool * Toplevel.state) lazy Inttab.table,  (*exec_id -> execution process*)
   133   execution: unit future list}  (*global execution process*)
   134 with
   135 
   136 fun make_state (versions, commands, execs, execution) =
   137   State {versions = versions, commands = commands, execs = execs, execution = execution};
   138 
   139 fun map_state f (State {versions, commands, execs, execution}) =
   140   make_state (f (versions, commands, execs, execution));
   141 
   142 val init_state =
   143   make_state (Inttab.make [(no_id, empty_version)],
   144     Inttab.make [(no_id, Future.value Toplevel.empty)],
   145     Inttab.make [(no_id, Lazy.value (true, Toplevel.toplevel))],
   146     []);
   147 
   148 
   149 (* document versions *)
   150 
   151 fun define_version (id: version_id) version =
   152   map_state (fn (versions, commands, execs, execution) =>
   153     let val versions' = Inttab.update_new (id, version) versions
   154       handle Inttab.DUP dup => err_dup "document version" dup
   155     in (versions', commands, execs, execution) end);
   156 
   157 fun the_version (State {versions, ...}) (id: version_id) =
   158   (case Inttab.lookup versions id of
   159     NONE => err_undef "document version" id
   160   | SOME version => version);
   161 
   162 
   163 (* commands *)
   164 
   165 fun define_command (id: command_id) text =
   166   map_state (fn (versions, commands, execs, execution) =>
   167     let
   168       val id_string = print_id id;
   169       val tr = Future.fork_pri 2 (fn () =>
   170         Position.setmp_thread_data (Position.id_only id_string)
   171           (fn () => Outer_Syntax.prepare_command (Position.id id_string) text) ());
   172       val commands' =
   173         Inttab.update_new (id, tr) commands
   174           handle Inttab.DUP dup => err_dup "command" dup;
   175     in (versions, commands', execs, execution) end);
   176 
   177 fun the_command (State {commands, ...}) (id: command_id) =
   178   (case Inttab.lookup commands id of
   179     NONE => err_undef "command" id
   180   | SOME tr => tr);
   181 
   182 fun join_commands (State {commands, ...}) =
   183   Inttab.fold (fn (_, tr) => fn () => ignore (Future.join_result tr)) commands ();
   184 
   185 
   186 (* command executions *)
   187 
   188 fun define_exec (id: exec_id) exec =
   189   map_state (fn (versions, commands, execs, execution) =>
   190     let val execs' = Inttab.update_new (id, exec) execs
   191       handle Inttab.DUP dup => err_dup "command execution" dup
   192     in (versions, commands, execs', execution) end);
   193 
   194 fun the_exec (State {execs, ...}) (id: exec_id) =
   195   (case Inttab.lookup execs id of
   196     NONE => err_undef "command execution" id
   197   | SOME exec => exec);
   198 
   199 fun get_theory state version_id pos name =
   200   let
   201     val last = get_last (get_node (the_version state version_id) name);
   202     val st = #2 (Lazy.force (the_exec state last));
   203   in Toplevel.end_theory pos st end;
   204 
   205 
   206 (* document execution *)
   207 
   208 fun cancel_execution (State {execution, ...}) =
   209   (List.app Future.cancel execution;
   210     fn () => ignore (Future.join_results execution));
   211 
   212 end;
   213 
   214 
   215 
   216 (* toplevel transactions *)
   217 
   218 local
   219 
   220 fun timing tr t = Toplevel.status tr (Markup.timing t);
   221 
   222 fun proof_status tr st =
   223   (case try Toplevel.proof_of st of
   224     SOME prf => Toplevel.status tr (Proof.status_markup prf)
   225   | NONE => ());
   226 
   227 fun async_state tr st =
   228   ignore
   229     (singleton
   230       (Future.forks {name = "Document.async_state",
   231         group = SOME (Task_Queue.new_group NONE), deps = [], pri = 0})
   232       (fn () =>
   233         Toplevel.setmp_thread_position tr
   234           (fn () => Toplevel.print_state false st) ()));
   235 
   236 fun run int tr st =
   237   (case Toplevel.transition int tr st of
   238     SOME (st', NONE) => ([], SOME st')
   239   | SOME (_, SOME exn_info) =>
   240       (case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of
   241         [] => Exn.interrupt ()
   242       | errs => (errs, NONE))
   243   | NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE));
   244 
   245 in
   246 
   247 fun run_command thy_name raw_tr st =
   248   (case
   249       (case Toplevel.init_of raw_tr of
   250         SOME name => Exn.capture (fn () =>
   251           let
   252             val path = Path.explode thy_name;
   253             val _ = Thy_Header.consistent_name (Path.implode (Path.base path)) name;
   254           in Toplevel.modify_master (SOME (Path.dir path)) raw_tr end) ()
   255       | NONE => Exn.Res raw_tr) of
   256     Exn.Res tr =>
   257       let
   258         val is_init = is_some (Toplevel.init_of tr);
   259         val is_proof = Keyword.is_proof (Toplevel.name_of tr);
   260         val do_print = not is_init andalso (Toplevel.print_of tr orelse is_proof);
   261 
   262         val start = Timing.start ();
   263         val (errs, result) =
   264           if Toplevel.is_toplevel st andalso not is_init then ([], SOME st)
   265           else run (is_init orelse is_proof) (Toplevel.set_print false tr) st;
   266         val _ = timing tr (Timing.result start);
   267         val _ = List.app (Toplevel.error_msg tr) errs;
   268         val res =
   269           (case result of
   270             NONE => (Toplevel.status tr Markup.failed; (false, st))
   271           | SOME st' =>
   272              (Toplevel.status tr Markup.finished;
   273               proof_status tr st';
   274               if do_print then async_state tr st' else ();
   275               (true, st')));
   276       in res end
   277   | Exn.Exn exn =>
   278       if Exn.is_interrupt exn then reraise exn
   279       else
   280        (Toplevel.error_msg raw_tr (ML_Compiler.exn_message exn);
   281         Toplevel.status raw_tr Markup.failed;
   282         (false, Toplevel.toplevel)));
   283 
   284 end;
   285 
   286 
   287 
   288 
   289 (** editing **)
   290 
   291 (* edit *)
   292 
   293 local
   294 
   295 fun is_changed node' ((_, id), exec) =
   296   (case try (the_entry node') id of
   297     NONE => true
   298   | SOME exec' => exec' <> exec);
   299 
   300 fun new_exec name (id: command_id) (exec_id, updates, state) =
   301   let
   302     val exec = the_exec state exec_id;
   303     val exec_id' = new_id ();
   304     val future_tr = the_command state id;
   305     val exec' =
   306       Lazy.lazy (fn () =>
   307         let
   308           val st = #2 (Lazy.force exec);
   309           val exec_tr = Toplevel.put_id (print_id exec_id') (Future.join future_tr);
   310         in run_command name exec_tr st end);
   311     val state' = define_exec exec_id' exec' state;
   312   in (exec_id', (id, exec_id') :: updates, state') end;
   313 
   314 in
   315 
   316 fun edit (old_id: version_id) (new_id: version_id) edits headers state =
   317   let
   318     (* FIXME apply headers *)
   319 
   320     val old_version = the_version state old_id;
   321     val _ = Time.now ();  (* FIXME odd workaround *)
   322     val new_version = fold edit_nodes edits old_version;
   323 
   324     fun update_node name (rev_updates, version, st) =
   325       let val node = get_node version name in
   326         (case first_entry NONE (is_changed (get_node old_version name)) node of
   327           NONE => (rev_updates, version, st)
   328         | SOME ((prev, id), _) =>
   329             let
   330               val prev_exec =
   331                 (case prev of
   332                   NONE => no_id
   333                 | SOME prev_id => the_default no_id (the_entry node prev_id));
   334               val (last, rev_upds, st') =
   335                 fold_entries (SOME id) (new_exec name o #2 o #1) node (prev_exec, [], st);
   336               val node' = node |> fold update_entry rev_upds |> set_last last;
   337             in (rev_upds @ rev_updates, put_node name node' version, st') end)
   338       end;
   339 
   340     (* FIXME proper node deps *)
   341     val (rev_updates, new_version', state') =
   342       fold update_node (node_names_of new_version) ([], new_version, state);
   343     val state'' = define_version new_id new_version' state';
   344 
   345     val _ = join_commands state'';  (* FIXME async!? *)
   346   in (rev rev_updates, state'') end;
   347 
   348 end;
   349 
   350 
   351 (* execute *)
   352 
   353 fun execute version_id state =
   354   state |> map_state (fn (versions, commands, execs, _) =>
   355     let
   356       val version = the_version state version_id;
   357 
   358       fun force_exec NONE = ()
   359         | force_exec (SOME exec_id) = ignore (Lazy.force (the_exec state exec_id));
   360 
   361       val execution' = (* FIXME proper node deps *)
   362         Future.forks {name = "Document.execute", group = NONE, deps = [], pri = 1}
   363           [fn () =>
   364             node_names_of version |> List.app (fn name =>
   365               fold_entries NONE (fn (_, exec) => fn () => force_exec exec)
   366                   (get_node version name) ())];
   367 
   368     in (versions, commands, execs, execution') end);
   369 
   370 
   371 
   372 (** global state **)
   373 
   374 val global_state = Synchronized.var "Document" init_state;
   375 
   376 fun state () = Synchronized.value global_state;
   377 val change_state = Synchronized.change global_state;
   378 
   379 end;
   380