src/Pure/PIDE/document.ML
changeset 66379 6392766f3c25
parent 66369 d003b44674c1
child 67215 03d0c958d65a
     1.1 --- a/src/Pure/PIDE/document.ML	Tue Aug 08 12:21:29 2017 +0200
     1.2 +++ b/src/Pure/PIDE/document.ML	Tue Aug 08 22:13:05 2017 +0200
     1.3 @@ -24,6 +24,7 @@
     1.4    val command_exec: state -> string -> Document_ID.command -> Command.exec option
     1.5    val remove_versions: Document_ID.version list -> state -> state
     1.6    val start_execution: state -> state
     1.7 +  val consolidate_execution: state -> unit
     1.8    val update: Document_ID.version -> Document_ID.version -> edit list -> state ->
     1.9      Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state
    1.10    val state: unit -> state
    1.11 @@ -59,16 +60,17 @@
    1.12    keywords: Keyword.keywords option,  (*outer syntax keywords*)
    1.13    perspective: perspective,  (*command perspective*)
    1.14    entries: Command.exec option Entries.T,  (*command entries with executions*)
    1.15 -  result: Command.eval option}  (*result of last execution*)
    1.16 +  result: Command.eval option,  (*result of last execution*)
    1.17 +  consolidated: unit lazy}  (*consolidation status of eval forks*)
    1.18  and version = Version of node String_Graph.T  (*development graph wrt. static imports*)
    1.19  with
    1.20  
    1.21 -fun make_node (header, keywords, perspective, entries, result) =
    1.22 +fun make_node (header, keywords, perspective, entries, result, consolidated) =
    1.23    Node {header = header, keywords = keywords, perspective = perspective,
    1.24 -    entries = entries, result = result};
    1.25 +    entries = entries, result = result, consolidated = consolidated};
    1.26  
    1.27 -fun map_node f (Node {header, keywords, perspective, entries, result}) =
    1.28 -  make_node (f (header, keywords, perspective, entries, result));
    1.29 +fun map_node f (Node {header, keywords, perspective, entries, result, consolidated}) =
    1.30 +  make_node (f (header, keywords, perspective, entries, result, consolidated));
    1.31  
    1.32  fun make_perspective (required, command_ids, overlays) : perspective =
    1.33   {required = required,
    1.34 @@ -80,7 +82,7 @@
    1.35    {master = "", header = Thy_Header.make ("", Position.none) [] [], errors = []};
    1.36  val no_perspective = make_perspective (false, [], []);
    1.37  
    1.38 -val empty_node = make_node (no_header, NONE, no_perspective, Entries.empty, NONE);
    1.39 +val empty_node = make_node (no_header, NONE, no_perspective, Entries.empty, NONE, Lazy.value ());
    1.40  
    1.41  fun is_no_perspective ({required, visible, visible_last, overlays}: perspective) =
    1.42    not required andalso
    1.43 @@ -88,12 +90,13 @@
    1.44    is_none visible_last andalso
    1.45    Inttab.is_empty overlays;
    1.46  
    1.47 -fun is_empty_node (Node {header, keywords, perspective, entries, result}) =
    1.48 +fun is_empty_node (Node {header, keywords, perspective, entries, result, consolidated}) =
    1.49    header = no_header andalso
    1.50    is_none keywords andalso
    1.51    is_no_perspective perspective andalso
    1.52    Entries.is_empty entries andalso
    1.53 -  is_none result;
    1.54 +  is_none result andalso
    1.55 +  Lazy.is_finished consolidated;
    1.56  
    1.57  
    1.58  (* basic components *)
    1.59 @@ -104,14 +107,15 @@
    1.60    | _ => Path.current);
    1.61  
    1.62  fun set_header master header errors =
    1.63 -  map_node (fn (_, keywords, perspective, entries, result) =>
    1.64 -    ({master = master, header = header, errors = errors}, keywords, perspective, entries, result));
    1.65 +  map_node (fn (_, keywords, perspective, entries, result, consolidated) =>
    1.66 +    ({master = master, header = header, errors = errors},
    1.67 +      keywords, perspective, entries, result, consolidated));
    1.68  
    1.69  fun get_header (Node {header, ...}) = header;
    1.70  
    1.71  fun set_keywords keywords =
    1.72 -  map_node (fn (header, _, perspective, entries, result) =>
    1.73 -    (header, keywords, perspective, entries, result));
    1.74 +  map_node (fn (header, _, perspective, entries, result, consolidated) =>
    1.75 +    (header, keywords, perspective, entries, result, consolidated));
    1.76  
    1.77  fun get_keywords (Node {keywords, ...}) = keywords;
    1.78  
    1.79 @@ -134,8 +138,8 @@
    1.80  fun get_perspective (Node {perspective, ...}) = perspective;
    1.81  
    1.82  fun set_perspective args =
    1.83 -  map_node (fn (header, keywords, _, entries, result) =>
    1.84 -    (header, keywords, make_perspective args, entries, result));
    1.85 +  map_node (fn (header, keywords, _, entries, result, consolidated) =>
    1.86 +    (header, keywords, make_perspective args, entries, result, consolidated));
    1.87  
    1.88  val required_node = #required o get_perspective;
    1.89  val visible_command = Inttab.defined o #visible o get_perspective;
    1.90 @@ -144,8 +148,8 @@
    1.91  val overlays = Inttab.lookup_list o #overlays o get_perspective;
    1.92  
    1.93  fun map_entries f =
    1.94 -  map_node (fn (header, keywords, perspective, entries, result) =>
    1.95 -    (header, keywords, perspective, f entries, result));
    1.96 +  map_node (fn (header, keywords, perspective, entries, result, consolidated) =>
    1.97 +    (header, keywords, perspective, f entries, result, consolidated));
    1.98  
    1.99  fun get_entries (Node {entries, ...}) = entries;
   1.100  
   1.101 @@ -158,14 +162,8 @@
   1.102  fun get_result (Node {result, ...}) = result;
   1.103  
   1.104  fun set_result result =
   1.105 -  map_node (fn (header, keywords, perspective, entries, _) =>
   1.106 -    (header, keywords, perspective, entries, result));
   1.107 -
   1.108 -fun changed_result node node' =
   1.109 -  (case (get_result node, get_result node') of
   1.110 -    (SOME eval, SOME eval') => not (Command.eval_eq (eval, eval'))
   1.111 -  | (NONE, NONE) => false
   1.112 -  | _ => true);
   1.113 +  map_node (fn (header, keywords, perspective, entries, _, consolidated) =>
   1.114 +    (header, keywords, perspective, entries, result, consolidated));
   1.115  
   1.116  fun pending_result node =
   1.117    (case get_result node of
   1.118 @@ -177,6 +175,35 @@
   1.119      SOME eval => Command.eval_finished eval
   1.120    | NONE => false);
   1.121  
   1.122 +fun finished_result_theory node =
   1.123 +  finished_result node andalso
   1.124 +    let val st = Command.eval_result_state (the (get_result node))
   1.125 +    in (Toplevel.end_theory Position.none st; true) handle ERROR _ => false end;
   1.126 +
   1.127 +val reset_consolidated =
   1.128 +  map_node (fn (header, keywords, perspective, entries, result, _) =>
   1.129 +    (header, keywords, perspective, entries, result, Lazy.lazy I));
   1.130 +
   1.131 +fun check_consolidated (node as Node {consolidated, ...}) =
   1.132 +  Lazy.is_finished consolidated orelse
   1.133 +  finished_result_theory node andalso
   1.134 +    let
   1.135 +      val result_id = Command.eval_exec_id (the (get_result node));
   1.136 +      val eval_ids =
   1.137 +        iterate_entries (fn (_, opt_exec) => fn eval_ids =>
   1.138 +          (case opt_exec of
   1.139 +            SOME (eval, _) => SOME (cons (Command.eval_exec_id eval) eval_ids)
   1.140 +          | NONE => NONE)) node [];
   1.141 +    in
   1.142 +      (case Execution.snapshot eval_ids of
   1.143 +        [] =>
   1.144 +         (Lazy.force consolidated;
   1.145 +          Position.setmp_thread_data (Position.id_only (Document_ID.print result_id))
   1.146 +            (fn () => Output.status (Markup.markup_only Markup.consolidated)) ();
   1.147 +          true)
   1.148 +      | _ => false)
   1.149 +    end;
   1.150 +
   1.151  fun get_node nodes name = String_Graph.get_node nodes name
   1.152    handle String_Graph.UNDEF _ => empty_node;
   1.153  fun default_node name = String_Graph.default_node (name, empty_node);
   1.154 @@ -400,10 +427,16 @@
   1.155  
   1.156  val the_command_name = #1 oo the_command;
   1.157  
   1.158 +
   1.159 +(* execution *)
   1.160 +
   1.161 +fun get_execution (State {execution, ...}) = execution;
   1.162 +fun get_execution_version state = the_version state (#version_id (get_execution state));
   1.163 +
   1.164  fun command_exec state node_name command_id =
   1.165    let
   1.166 -    val State {execution = {version_id, ...}, ...} = state;
   1.167 -    val node = get_node (nodes_of (the_version state version_id)) node_name;
   1.168 +    val version = get_execution_version state;
   1.169 +    val node = get_node (nodes_of version) node_name;
   1.170    in the_entry node command_id end;
   1.171  
   1.172  end;
   1.173 @@ -492,6 +525,10 @@
   1.174          {version_id = version_id, execution_id = execution_id, delay_request = delay_request'};
   1.175      in (versions, blobs, commands, execution') end));
   1.176  
   1.177 +fun consolidate_execution state =
   1.178 +  String_Graph.fold (fn (_, (node, _)) => fn () => ignore (check_consolidated node))
   1.179 +    (nodes_of (get_execution_version state)) ();
   1.180 +
   1.181  
   1.182  
   1.183  (** document update **)
   1.184 @@ -702,11 +739,13 @@
   1.185                          val removed = maps (removed_execs node0) assign_update;
   1.186                          val _ = List.app Execution.cancel removed;
   1.187  
   1.188 +                        val result_changed =
   1.189 +                          not (eq_option Command.eval_eq (get_result node0, result));
   1.190                          val node' = node
   1.191                            |> assign_update_apply assigned_execs
   1.192 -                          |> set_result result;
   1.193 +                          |> set_result result
   1.194 +                          |> result_changed ? reset_consolidated;
   1.195                          val assigned_node = SOME (name, node');
   1.196 -                        val result_changed = changed_result node0 node';
   1.197                        in ((removed, assign_update, assigned_node, result_changed), node') end
   1.198                      else (([], [], NONE, false), node)
   1.199                    end))))