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