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