clarified "consolidation" vs. "presentation";
authorwenzelm
Wed May 16 21:07:12 2018 +0200 (12 months ago)
changeset 681977857817403e4
parent 68196 756434c77d21
child 68198 6710167e17af
clarified "consolidation" vs. "presentation";
etc/options
src/Pure/PIDE/document.ML
     1.1 --- a/etc/options	Wed May 16 21:06:28 2018 +0200
     1.2 +++ b/etc/options	Wed May 16 21:07:12 2018 +0200
     1.3 @@ -189,8 +189,8 @@
     1.4  option editor_syslog_limit : int = 100
     1.5    -- "maximum amount of buffered syslog messages"
     1.6  
     1.7 -public option editor_document_output : bool = false
     1.8 -  -- "dynamic document output while editing"
     1.9 +public option editor_presentation : bool = false
    1.10 +  -- "dynamic presentation while editing"
    1.11  
    1.12  
    1.13  section "Miscellaneous Tools"
     2.1 --- a/src/Pure/PIDE/document.ML	Wed May 16 21:06:28 2018 +0200
     2.2 +++ b/src/Pure/PIDE/document.ML	Wed May 16 21:07:12 2018 +0200
     2.3 @@ -55,22 +55,24 @@
     2.4  
     2.5  structure Entries = Linear_Set(type key = Document_ID.command val ord = int_ord);
     2.6  
     2.7 +type consolidation = (int -> int option) * Thy_Output.segment list;
     2.8 +
     2.9  abstype node = Node of
    2.10   {header: node_header,  (*master directory, theory header, errors*)
    2.11    keywords: Keyword.keywords option,  (*outer syntax keywords*)
    2.12    perspective: perspective,  (*command perspective*)
    2.13    entries: Command.exec option Entries.T,  (*command entries with executions*)
    2.14    result: Command.eval option,  (*result of last execution*)
    2.15 -  consolidated: unit lazy}  (*consolidation status of eval forks*)
    2.16 +  consolidation: consolidation future}  (*consolidation status of eval forks*)
    2.17  and version = Version of node String_Graph.T  (*development graph wrt. static imports*)
    2.18  with
    2.19  
    2.20 -fun make_node (header, keywords, perspective, entries, result, consolidated) =
    2.21 +fun make_node (header, keywords, perspective, entries, result, consolidation) =
    2.22    Node {header = header, keywords = keywords, perspective = perspective,
    2.23 -    entries = entries, result = result, consolidated = consolidated};
    2.24 +    entries = entries, result = result, consolidation = consolidation};
    2.25  
    2.26 -fun map_node f (Node {header, keywords, perspective, entries, result, consolidated}) =
    2.27 -  make_node (f (header, keywords, perspective, entries, result, consolidated));
    2.28 +fun map_node f (Node {header, keywords, perspective, entries, result, consolidation}) =
    2.29 +  make_node (f (header, keywords, perspective, entries, result, consolidation));
    2.30  
    2.31  fun make_perspective (required, command_ids, overlays) : perspective =
    2.32   {required = required,
    2.33 @@ -82,7 +84,8 @@
    2.34    {master = "", header = Thy_Header.make ("", Position.none) [] [], errors = []};
    2.35  val no_perspective = make_perspective (false, [], []);
    2.36  
    2.37 -val empty_node = make_node (no_header, NONE, no_perspective, Entries.empty, NONE, Lazy.value ());
    2.38 +val empty_node =
    2.39 +  make_node (no_header, NONE, no_perspective, Entries.empty, NONE, Future.value (K NONE, []));
    2.40  
    2.41  fun is_no_perspective ({required, visible, visible_last, overlays}: perspective) =
    2.42    not required andalso
    2.43 @@ -90,13 +93,13 @@
    2.44    is_none visible_last andalso
    2.45    Inttab.is_empty overlays;
    2.46  
    2.47 -fun is_empty_node (Node {header, keywords, perspective, entries, result, consolidated}) =
    2.48 +fun is_empty_node (Node {header, keywords, perspective, entries, result, consolidation}) =
    2.49    header = no_header andalso
    2.50    is_none keywords andalso
    2.51    is_no_perspective perspective andalso
    2.52    Entries.is_empty entries andalso
    2.53    is_none result andalso
    2.54 -  Lazy.is_finished consolidated;
    2.55 +  Future.is_finished consolidation;
    2.56  
    2.57  
    2.58  (* basic components *)
    2.59 @@ -107,15 +110,15 @@
    2.60    | _ => Path.current);
    2.61  
    2.62  fun set_header master header errors =
    2.63 -  map_node (fn (_, keywords, perspective, entries, result, consolidated) =>
    2.64 +  map_node (fn (_, keywords, perspective, entries, result, consolidation) =>
    2.65      ({master = master, header = header, errors = errors},
    2.66 -      keywords, perspective, entries, result, consolidated));
    2.67 +      keywords, perspective, entries, result, consolidation));
    2.68  
    2.69  fun get_header (Node {header, ...}) = header;
    2.70  
    2.71  fun set_keywords keywords =
    2.72 -  map_node (fn (header, _, perspective, entries, result, consolidated) =>
    2.73 -    (header, keywords, perspective, entries, result, consolidated));
    2.74 +  map_node (fn (header, _, perspective, entries, result, consolidation) =>
    2.75 +    (header, keywords, perspective, entries, result, consolidation));
    2.76  
    2.77  fun get_keywords (Node {keywords, ...}) = keywords;
    2.78  
    2.79 @@ -139,8 +142,8 @@
    2.80  fun get_perspective (Node {perspective, ...}) = perspective;
    2.81  
    2.82  fun set_perspective args =
    2.83 -  map_node (fn (header, keywords, _, entries, result, consolidated) =>
    2.84 -    (header, keywords, make_perspective args, entries, result, consolidated));
    2.85 +  map_node (fn (header, keywords, _, entries, result, consolidation) =>
    2.86 +    (header, keywords, make_perspective args, entries, result, consolidation));
    2.87  
    2.88  val required_node = #required o get_perspective;
    2.89  val visible_command = Inttab.defined o #visible o get_perspective;
    2.90 @@ -149,8 +152,8 @@
    2.91  val overlays = Inttab.lookup_list o #overlays o get_perspective;
    2.92  
    2.93  fun map_entries f =
    2.94 -  map_node (fn (header, keywords, perspective, entries, result, consolidated) =>
    2.95 -    (header, keywords, perspective, f entries, result, consolidated));
    2.96 +  map_node (fn (header, keywords, perspective, entries, result, consolidation) =>
    2.97 +    (header, keywords, perspective, f entries, result, consolidation));
    2.98  
    2.99  fun get_entries (Node {entries, ...}) = entries;
   2.100  
   2.101 @@ -163,8 +166,8 @@
   2.102  fun get_result (Node {result, ...}) = result;
   2.103  
   2.104  fun set_result result =
   2.105 -  map_node (fn (header, keywords, perspective, entries, _, consolidated) =>
   2.106 -    (header, keywords, perspective, entries, result, consolidated));
   2.107 +  map_node (fn (header, keywords, perspective, entries, _, consolidation) =>
   2.108 +    (header, keywords, perspective, entries, result, consolidation));
   2.109  
   2.110  fun pending_result node =
   2.111    (case get_result node of
   2.112 @@ -182,11 +185,11 @@
   2.113      in SOME (Toplevel.end_theory Position.none st) handle ERROR _ => NONE end
   2.114    else NONE;
   2.115  
   2.116 -val reset_consolidated =
   2.117 +val reset_consolidation =
   2.118    map_node (fn (header, keywords, perspective, entries, result, _) =>
   2.119 -    (header, keywords, perspective, entries, result, Lazy.lazy I));
   2.120 +    (header, keywords, perspective, entries, result, Future.promise I));
   2.121  
   2.122 -fun get_consolidated (Node {consolidated, ...}) = consolidated;
   2.123 +fun get_consolidation (Node {consolidation, ...}) = consolidation;
   2.124  
   2.125  fun get_node nodes name = String_Graph.get_node nodes name
   2.126    handle String_Graph.UNDEF _ => empty_node;
   2.127 @@ -512,10 +515,22 @@
   2.128          {version_id = version_id, execution_id = execution_id, delay_request = delay_request'};
   2.129      in (versions, blobs, commands, execution') end));
   2.130  
   2.131 +fun presentation options thy node_name node =
   2.132 +  if Options.bool options "editor_presentation" then
   2.133 +    let
   2.134 +      val (adjust, segments) = Future.get_finished (get_consolidation node);
   2.135 +      val presentation_context: Thy_Info.presentation_context =
   2.136 +       {options = options,
   2.137 +        file_pos = Position.file node_name,
   2.138 +        adjust_pos = Position.adjust_offsets adjust,
   2.139 +        segments = segments};
   2.140 +    in Thy_Info.apply_presentation presentation_context thy end
   2.141 +  else ();
   2.142 +
   2.143  fun consolidate_execution state =
   2.144    let
   2.145 -    fun check_consolidated node_name node =
   2.146 -      if Lazy.is_finished (get_consolidated node) then ()
   2.147 +    fun check_consolidation node_name node =
   2.148 +      if Future.is_finished (get_consolidation node) then ()
   2.149        else
   2.150          (case finished_result_theory node of
   2.151            NONE => ()
   2.152 @@ -552,31 +567,22 @@
   2.153                          | NONE => NONE)) node (0, Inttab.empty, []);
   2.154  
   2.155                      val adjust = Inttab.lookup offsets;
   2.156 -                    val adjust_pos = Position.adjust_offsets adjust;
   2.157 -                    val adjust_token = Token.adjust_offsets adjust;
   2.158                      val segments =
   2.159                        rev rev_segments |> map (fn (span, tr, st') =>
   2.160                          {span = Command_Span.adjust_offsets adjust span, command = tr, state = st'});
   2.161  
   2.162 -                    val presentation_context: Thy_Info.presentation_context =
   2.163 -                     {options = Options.default (),
   2.164 -                      file_pos = Position.file node_name,
   2.165 -                      adjust_pos = adjust_pos,
   2.166 -                      segments = segments};
   2.167 -
   2.168 -                    val _ = Lazy.force (get_consolidated node);
   2.169 +                    val _ = Future.fulfill (get_consolidation node) (adjust, segments);
   2.170                      val _ =
   2.171                        Position.setmp_thread_data (Position.id_only (Document_ID.print result_id))
   2.172                          (fn () =>
   2.173 -                          (if Options.default_bool "editor_document_output" then
   2.174 -                            Thy_Info.apply_presentation presentation_context thy (* FIXME errors!? *)
   2.175 -                           else ();
   2.176 -                           Output.status (Markup.markup_only Markup.consolidated))) ();
   2.177 +                          (Output.status (Markup.markup_only Markup.consolidated);
   2.178 +                            (* FIXME avoid user operations on protocol thread *)
   2.179 +                            presentation (Options.default ()) thy node_name node)) ();
   2.180                    in () end
   2.181                | _ => ())
   2.182              end);
   2.183        in
   2.184 -        String_Graph.fold (fn (node_name, (node, _)) => fn () => check_consolidated node_name node)
   2.185 +        String_Graph.fold (fn (node_name, (node, _)) => fn () => check_consolidation node_name node)
   2.186            (nodes_of (get_execution_version state)) ()
   2.187        end;
   2.188  
   2.189 @@ -799,7 +805,7 @@
   2.190                          val node' = node
   2.191                            |> assign_update_apply assigned_execs
   2.192                            |> set_result result
   2.193 -                          |> result_changed ? reset_consolidated;
   2.194 +                          |> result_changed ? reset_consolidation;
   2.195                          val assigned_node = SOME (name, node');
   2.196                        in ((removed, assign_update, assigned_node, result_changed), node') end
   2.197                      else (([], [], NONE, false), node)