less agressive parsing of commands (priority ~1);
authorwenzelm
Fri Sep 02 21:06:05 2011 +0200 (2011-09-02 ago)
changeset 4466090bab3febb6c
parent 44659 665ebb45bc1a
child 44661 383c9d758a56
less agressive parsing of commands (priority ~1);
join commands just before actual assignment;
src/Pure/PIDE/document.ML
src/Pure/PIDE/isar_document.ML
     1.1 --- a/src/Pure/PIDE/document.ML	Fri Sep 02 20:35:32 2011 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Fri Sep 02 21:06:05 2011 +0200
     1.3 @@ -25,7 +25,6 @@
     1.4    type state
     1.5    val init_state: state
     1.6    val define_command: command_id -> string -> string -> state -> state
     1.7 -  val join_commands: state -> state
     1.8    val cancel_execution: state -> Future.task list
     1.9    val update_perspective: version_id -> version_id -> string -> command_id list -> state -> state
    1.10    val update: version_id -> version_id -> edit list -> state ->
    1.11 @@ -237,9 +236,7 @@
    1.12  
    1.13  abstype state = State of
    1.14   {versions: version Inttab.table,  (*version_id -> document content*)
    1.15 -  commands:
    1.16 -    (string * Toplevel.transition future) Inttab.table *  (*command_id -> name * transition*)
    1.17 -    Toplevel.transition future list,  (*recent commands to be joined*)
    1.18 +  commands: (string * Toplevel.transition future) Inttab.table,  (*command_id -> name * transition*)
    1.19    execs: (command_id * (Toplevel.state * unit lazy) lazy) Inttab.table,
    1.20      (*exec_id -> command_id with eval/print process*)
    1.21    execution: Future.group}  (*global execution process*)
    1.22 @@ -253,7 +250,7 @@
    1.23  
    1.24  val init_state =
    1.25    make_state (Inttab.make [(no_id, empty_version)],
    1.26 -    (Inttab.make [(no_id, (Toplevel.name_of Toplevel.empty, Future.value Toplevel.empty))], []),
    1.27 +    Inttab.make [(no_id, (Toplevel.name_of Toplevel.empty, Future.value Toplevel.empty))],
    1.28      Inttab.make [(no_id, (no_id, Lazy.value (Toplevel.toplevel, no_print)))],
    1.29      Future.new_group NONE);
    1.30  
    1.31 @@ -275,27 +272,26 @@
    1.32  (* commands *)
    1.33  
    1.34  fun define_command (id: command_id) name text =
    1.35 -  map_state (fn (versions, (commands, recent), execs, execution) =>
    1.36 +  map_state (fn (versions, commands, execs, execution) =>
    1.37      let
    1.38        val id_string = print_id id;
    1.39 -      val tr =
    1.40 -        Future.fork_pri 2 (fn () =>
    1.41 -          Position.setmp_thread_data (Position.id_only id_string)
    1.42 -            (fn () => Outer_Syntax.read_command (Position.id id_string) text) ());
    1.43 +      val future =
    1.44 +        (singleton o Future.forks)
    1.45 +          {name = "Document.define_command", group = SOME (Future.new_group NONE),
    1.46 +            deps = [], pri = ~1, interrupts = false}
    1.47 +          (fn () =>
    1.48 +            Position.setmp_thread_data (Position.id_only id_string)
    1.49 +              (fn () => Outer_Syntax.read_command (Position.id id_string) text) ());
    1.50        val commands' =
    1.51 -        Inttab.update_new (id, (name, tr)) commands
    1.52 +        Inttab.update_new (id, (name, future)) commands
    1.53            handle Inttab.DUP dup => err_dup "command" dup;
    1.54 -    in (versions, (commands', tr :: recent), execs, execution) end);
    1.55 +    in (versions, commands', execs, execution) end);
    1.56  
    1.57  fun the_command (State {commands, ...}) (id: command_id) =
    1.58 -  (case Inttab.lookup (#1 commands) id of
    1.59 +  (case Inttab.lookup commands id of
    1.60      NONE => err_undef "command" id
    1.61    | SOME command => command);
    1.62  
    1.63 -val join_commands =
    1.64 -    map_state (fn (versions, (commands, recent), execs, execution) =>
    1.65 -      (Future.join_results recent; (versions, (commands, []), execs, execution)));
    1.66 -
    1.67  
    1.68  (* command executions *)
    1.69  
    1.70 @@ -419,20 +415,16 @@
    1.71    if bad_init andalso is_none init then NONE
    1.72    else
    1.73      let
    1.74 -      val (name, tr0) = the_command state command_id';
    1.75 +      val (name, tr0) = the_command state command_id' ||> Future.join;
    1.76        val (modify_init, init') =
    1.77          if Keyword.is_theory_begin name then
    1.78            (Toplevel.modify_init (the_default illegal_init init), NONE)
    1.79          else (I, init);
    1.80 -        val exec_id' = new_id ();
    1.81 -      val exec' =
    1.82 -        snd exec |> Lazy.map (fn (st, _) =>
    1.83 -          let val tr =
    1.84 -            Future.join tr0
    1.85 -            |> modify_init
    1.86 -            |> Toplevel.put_id (print_id exec_id');
    1.87 -          in run_command tr st end)
    1.88 -        |> pair command_id';
    1.89 +      val exec_id' = new_id ();
    1.90 +      val tr = tr0
    1.91 +        |> modify_init
    1.92 +        |> Toplevel.put_id (print_id exec_id');
    1.93 +      val exec' = (command_id', Lazy.map (fn (st, _) => run_command tr st) (snd exec));
    1.94      in SOME ((exec_id', exec') :: execs, exec', init') end;
    1.95  
    1.96  fun make_required nodes =
     2.1 --- a/src/Pure/PIDE/isar_document.ML	Fri Sep 02 20:35:32 2011 +0200
     2.2 +++ b/src/Pure/PIDE/isar_document.ML	Fri Sep 02 21:06:05 2011 +0200
     2.3 @@ -55,15 +55,14 @@
     2.4          val running = Document.cancel_execution state;
     2.5          val (assignment, state1) = Document.update old_id new_id edits state;
     2.6          val _ = Future.join_tasks running;
     2.7 -        val state2 = Document.join_commands state1;
     2.8          val _ =
     2.9            Output.status (Markup.markup (Markup.assign new_id)
    2.10              (assignment |>
    2.11                let open XML.Encode
    2.12                in pair (list (pair int (option int))) (list (pair string (option int))) end
    2.13                |> YXML.string_of_body));
    2.14 -        val state3 = Document.execute new_id state2;
    2.15 -      in state3 end));
    2.16 +        val state2 = Document.execute new_id state1;
    2.17 +      in state2 end));
    2.18  
    2.19  val _ =
    2.20    Isabelle_Process.add_command "Isar_Document.invoke_scala"