# HG changeset patch # User wenzelm # Date 1527798433 -7200 # Node ID 09ac56914b299d5d6657a113888bd2dbd9413101 # Parent 2f080a51a10d8f8ae0e0f66525b2f5ae375a4e1a Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread; tuned; diff -r 2f080a51a10d -r 09ac56914b29 src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Thu May 31 22:10:06 2018 +0200 +++ b/src/Pure/PIDE/document.ML Thu May 31 22:27:13 2018 +0200 @@ -24,8 +24,7 @@ val command_exec: state -> string -> Document_ID.command -> Command.exec option val remove_versions: Document_ID.version list -> state -> state val start_execution: state -> state - val consolidate_execution: state -> unit - val update: Document_ID.version -> Document_ID.version -> edit list -> state -> + val update: Document_ID.version -> Document_ID.version -> edit list -> bool -> state -> Document_ID.exec list * (Document_ID.command * Document_ID.exec list) list * state val state: unit -> state val change_state: (state -> state) -> unit @@ -55,24 +54,22 @@ structure Entries = Linear_Set(type key = Document_ID.command val ord = int_ord); -type consolidation = (int -> int option) * Thy_Output.segment list; - abstype node = Node of {header: node_header, (*master directory, theory header, errors*) keywords: Keyword.keywords option, (*outer syntax keywords*) perspective: perspective, (*command perspective*) entries: Command.exec option Entries.T, (*command entries with executions*) - result: Command.eval option, (*result of last execution*) - consolidation: consolidation future} (*consolidation status of eval forks*) + result: (Document_ID.command * Command.eval) option, (*result of last execution*) + consolidated: unit lazy} (*consolidated status of eval forks*) and version = Version of node String_Graph.T (*development graph wrt. static imports*) with -fun make_node (header, keywords, perspective, entries, result, consolidation) = +fun make_node (header, keywords, perspective, entries, result, consolidated) = Node {header = header, keywords = keywords, perspective = perspective, - entries = entries, result = result, consolidation = consolidation}; + entries = entries, result = result, consolidated = consolidated}; -fun map_node f (Node {header, keywords, perspective, entries, result, consolidation}) = - make_node (f (header, keywords, perspective, entries, result, consolidation)); +fun map_node f (Node {header, keywords, perspective, entries, result, consolidated}) = + make_node (f (header, keywords, perspective, entries, result, consolidated)); fun make_perspective (required, command_ids, overlays) : perspective = {required = required, @@ -85,7 +82,7 @@ val no_perspective = make_perspective (false, [], []); val empty_node = - make_node (no_header, NONE, no_perspective, Entries.empty, NONE, Future.value (K NONE, [])); + make_node (no_header, NONE, no_perspective, Entries.empty, NONE, Lazy.value ()); fun is_no_perspective ({required, visible, visible_last, overlays}: perspective) = not required andalso @@ -93,13 +90,13 @@ is_none visible_last andalso Inttab.is_empty overlays; -fun is_empty_node (Node {header, keywords, perspective, entries, result, consolidation}) = +fun is_empty_node (Node {header, keywords, perspective, entries, result, consolidated}) = header = no_header andalso is_none keywords andalso is_no_perspective perspective andalso Entries.is_empty entries andalso is_none result andalso - Future.is_finished consolidation; + Lazy.is_finished consolidated; (* basic components *) @@ -110,15 +107,15 @@ | _ => Path.current); fun set_header master header errors = - map_node (fn (_, keywords, perspective, entries, result, consolidation) => + map_node (fn (_, keywords, perspective, entries, result, consolidated) => ({master = master, header = header, errors = errors}, - keywords, perspective, entries, result, consolidation)); + keywords, perspective, entries, result, consolidated)); fun get_header (Node {header, ...}) = header; fun set_keywords keywords = - map_node (fn (header, _, perspective, entries, result, consolidation) => - (header, keywords, perspective, entries, result, consolidation)); + map_node (fn (header, _, perspective, entries, result, consolidated) => + (header, keywords, perspective, entries, result, consolidated)); fun get_keywords (Node {keywords, ...}) = keywords; @@ -142,8 +139,8 @@ fun get_perspective (Node {perspective, ...}) = perspective; fun set_perspective args = - map_node (fn (header, keywords, _, entries, result, consolidation) => - (header, keywords, make_perspective args, entries, result, consolidation)); + map_node (fn (header, keywords, _, entries, result, consolidated) => + (header, keywords, make_perspective args, entries, result, consolidated)); val required_node = #required o get_perspective; val visible_command = Inttab.defined o #visible o get_perspective; @@ -152,8 +149,8 @@ val overlays = Inttab.lookup_list o #overlays o get_perspective; fun map_entries f = - map_node (fn (header, keywords, perspective, entries, result, consolidation) => - (header, keywords, perspective, f entries, result, consolidation)); + map_node (fn (header, keywords, perspective, entries, result, consolidated) => + (header, keywords, perspective, f entries, result, consolidated)); fun get_entries (Node {entries, ...}) = entries; @@ -166,30 +163,40 @@ fun get_result (Node {result, ...}) = result; fun set_result result = - map_node (fn (header, keywords, perspective, entries, _, consolidation) => - (header, keywords, perspective, entries, result, consolidation)); + map_node (fn (header, keywords, perspective, entries, _, consolidated) => + (header, keywords, perspective, entries, result, consolidated)); fun pending_result node = (case get_result node of - SOME eval => not (Command.eval_finished eval) + SOME (_, eval) => not (Command.eval_finished eval) | NONE => false); fun finished_result node = (case get_result node of - SOME eval => Command.eval_finished eval + SOME (_, eval) => Command.eval_finished eval | NONE => false); fun finished_result_theory node = if finished_result node then - let val st = Command.eval_result_state (the (get_result node)) - in SOME (Toplevel.end_theory Position.none st) handle ERROR _ => NONE end + let + val (result_id, eval) = the (get_result node); + val st = Command.eval_result_state eval; + in SOME (result_id, Toplevel.end_theory Position.none st) handle ERROR _ => NONE end else NONE; -val reset_consolidation = +val reset_consolidated = map_node (fn (header, keywords, perspective, entries, result, _) => - (header, keywords, perspective, entries, result, Future.promise I)); + (header, keywords, perspective, entries, result, Lazy.lazy I)); + +fun get_consolidated (Node {consolidated, ...}) = consolidated; + +val is_consolidated = Lazy.is_finished o get_consolidated; -fun get_consolidation (Node {consolidation, ...}) = consolidation; +fun commit_consolidated node = + (Lazy.force (get_consolidated node); Output.status (Markup.markup_only Markup.consolidated)); + +fun could_consolidate node = + not (is_consolidated node) andalso is_some (finished_result_theory node); fun get_node nodes name = String_Graph.get_node nodes name handle String_Graph.UNDEF _ => empty_node; @@ -414,9 +421,6 @@ val the_command_name = #1 oo the_command; -fun force_command_span state = - Outer_Syntax.make_span o Lazy.force o #4 o the_command state; - (* execution *) @@ -515,77 +519,6 @@ {version_id = version_id, execution_id = execution_id, delay_request = delay_request'}; in (versions, blobs, commands, execution') end)); -fun presentation options thy node_name node = - if Options.bool options "editor_presentation" then - let - val (adjust, segments) = Future.get_finished (get_consolidation node); - val presentation_context: Thy_Info.presentation_context = - {options = options, - file_pos = Position.file node_name, - adjust_pos = Position.adjust_offsets adjust, - segments = segments}; - in Thy_Info.apply_presentation presentation_context thy end - else (); - -fun consolidate_execution state = - let - fun check_consolidation node_name node = - if Future.is_finished (get_consolidation node) then () - else - (case finished_result_theory node of - NONE => () - | SOME thy => - let - val result_id = Command.eval_exec_id (the (get_result node)); - val eval_ids = - iterate_entries (fn (_, opt_exec) => fn eval_ids => - (case opt_exec of - SOME (eval, _) => SOME (cons (Command.eval_exec_id eval) eval_ids) - | NONE => NONE)) node []; - in - (case Execution.snapshot eval_ids of - [] => - let - val (_, offsets, rev_segments) = - iterate_entries (fn (_, opt_exec) => fn (offset, offsets, segments) => - (case opt_exec of - SOME (eval, _) => - let - val command_id = Command.eval_command_id eval; - val span = force_command_span state command_id; - - val exec_id = Command.eval_exec_id eval; - val tr = Command.eval_result_command eval; - val st' = Command.eval_result_state eval; - - val offset' = offset + the_default 0 (Command_Span.symbol_length span); - val offsets' = offsets - |> Inttab.update (command_id, offset) - |> Inttab.update (exec_id, offset); - val segments' = (span, tr, st') :: segments; - in SOME (offset', offsets', segments') end - | NONE => NONE)) node (0, Inttab.empty, []); - - val adjust = Inttab.lookup offsets; - val segments = - rev rev_segments |> map (fn (span, tr, st') => - {span = Command_Span.adjust_offsets adjust span, command = tr, state = st'}); - - val _ = Future.fulfill (get_consolidation node) (adjust, segments); - val _ = - Position.setmp_thread_data (Position.id_only (Document_ID.print result_id)) - (fn () => - (Output.status (Markup.markup_only Markup.consolidated); - (* FIXME avoid user operations on protocol thread *) - presentation (Options.default ()) thy node_name node)) (); - in () end - | _ => ()) - end); - in - String_Graph.fold (fn (node_name, (node, _)) => fn () => check_consolidation node_name node) - (nodes_of (get_execution_version state)) () - end; - (** document update **) @@ -596,6 +529,7 @@ val assign_update_empty: assign_update = Inttab.empty; fun assign_update_defined (tab: assign_update) command_id = Inttab.defined tab command_id; +fun assign_update_change entry (tab: assign_update) = Inttab.update entry tab; fun assign_update_apply (tab: assign_update) node = Inttab.fold assign_entry tab node; fun assign_update_new upd (tab: assign_update) = @@ -626,7 +560,7 @@ maybe_end_theory pos (case get_result (snd (the (AList.lookup (op =) deps import))) of NONE => Toplevel.toplevel - | SOME eval => Command.eval_result_state eval) + | SOME (_, eval) => Command.eval_result_state eval) | some => some) |> Option.map (fn thy => (thy, (pos, Theory.get_markup thy)))); @@ -727,10 +661,78 @@ fun removed_execs node0 (command_id, exec_ids) = subtract (op =) exec_ids (Command.exec_ids (lookup_entry node0 command_id)); +fun print_consolidation options the_command_span node_name (assign_update, node) = + (case finished_result_theory node of + SOME (result_id, thy) => + let + val eval_ids = + iterate_entries (fn (_, opt_exec) => fn eval_ids => + (case opt_exec of + SOME (eval, _) => SOME (cons (Command.eval_exec_id eval) eval_ids) + | NONE => NONE)) node []; + in + if null (Execution.snapshot eval_ids) then + let + val consolidation = + if Options.bool options "editor_presentation" then + let + val (_, offsets, rev_segments) = + iterate_entries (fn (_, opt_exec) => fn (offset, offsets, segments) => + (case opt_exec of + SOME (eval, _) => + let + val command_id = Command.eval_command_id eval; + val span = the_command_span command_id; + + val exec_id = Command.eval_exec_id eval; + val tr = Command.eval_result_command eval; + val st' = Command.eval_result_state eval; + + val offset' = offset + the_default 0 (Command_Span.symbol_length span); + val offsets' = offsets + |> Inttab.update (command_id, offset) + |> Inttab.update (exec_id, offset); + val segments' = (span, tr, st') :: segments; + in SOME (offset', offsets', segments') end + | NONE => NONE)) node (0, Inttab.empty, []); + + val adjust = Inttab.lookup offsets; + val segments = + rev rev_segments |> map (fn (span, tr, st') => + {span = Command_Span.adjust_offsets adjust span, command = tr, state = st'}); + + val presentation_context: Thy_Info.presentation_context = + {options = options, + file_pos = Position.file node_name, + adjust_pos = Position.adjust_offsets adjust, + segments = segments}; + in + fn () => + (Thy_Info.apply_presentation presentation_context thy; + commit_consolidated node) + end + else fn () => commit_consolidated node; + + val result_entry = + (case lookup_entry node result_id of + NONE => err_undef "result command entry" result_id + | SOME (eval, prints) => + (result_id, SOME (eval, Command.print0 consolidation eval :: prints))); + + val assign_update' = assign_update |> assign_update_change result_entry; + val node' = node |> assign_entry result_entry; + in (assign_update', node') end + else (assign_update, node) + end + | NONE => (assign_update, node)); in -fun update old_version_id new_version_id edits state = Runtime.exn_trace_system (fn () => +fun update old_version_id new_version_id edits consolidate state = + Runtime.exn_trace_system (fn () => let + val options = Options.default (); + val the_command_span = Outer_Syntax.make_span o Lazy.force o #4 o the_command state; + val old_version = the_version state old_version_id; val new_version = timeit "Document.edit_nodes" @@ -753,12 +755,15 @@ let val root_theory = check_root_theory node; val keywords = the_default (Session.get_keywords ()) (get_keywords node); + + val maybe_consolidate = consolidate andalso could_consolidate node; val imports = map (apsnd Future.join) deps; val imports_result_changed = exists (#4 o #1 o #2) imports; val node_required = Symtab.defined required name; in - if Symtab.defined edited name orelse visible_node node orelse - imports_result_changed orelse Symtab.defined required0 name <> node_required + if Symtab.defined edited name orelse maybe_consolidate orelse + visible_node node orelse imports_result_changed orelse + Symtab.defined required0 name <> node_required then let val node0 = node_of old_version name; @@ -785,7 +790,7 @@ if not node_required andalso prev = visible_last node then NONE else new_exec keywords state node proper_init id res) node; - val assigned_execs = + val assign_update = (node0, updated_execs) |-> iterate_entries_after common (fn ((_, command_id0), exec0) => fn res => if is_none exec0 then NONE @@ -796,32 +801,36 @@ if command_id' = Document_ID.none then NONE else SOME command_id'; val result = if is_none last_exec orelse is_some (after_entry node last_exec) then NONE - else SOME (#1 exec'); - - val assign_update = assign_update_result assigned_execs; - val removed = maps (removed_execs node0) assign_update; - val _ = List.app Execution.cancel removed; + else SOME (command_id', #1 exec'); val result_changed = - not (eq_option Command.eval_eq (get_result node0, result)); - val node' = node - |> assign_update_apply assigned_execs + not (eq_option (Command.eval_eq o apply2 #2) (get_result node0, result)); + val (assign_update', node') = node + |> assign_update_apply assign_update |> set_result result - |> result_changed ? reset_consolidation; + |> result_changed ? reset_consolidated + |> pair assign_update + |> (not result_changed andalso maybe_consolidate) ? + print_consolidation options the_command_span name; + + val assign_result = assign_update_result assign_update'; + val removed = maps (removed_execs node0) assign_result; + val _ = List.app Execution.cancel removed; + val assigned_node = SOME (name, node'); - in ((removed, assign_update, assigned_node, result_changed), node') end + in ((removed, assign_result, assigned_node, result_changed), node') end else (([], [], NONE, false), node) end)))) |> Future.joins |> map #1); val removed = maps #1 updated; - val assign_update = maps #2 updated; + val assign_result = maps #2 updated; val assigned_nodes = map_filter #3 updated; val state' = state |> define_version new_version_id (fold put_node assigned_nodes new_version); - in (removed, assign_update, state') end); + in (removed, assign_result, state') end); end; diff -r 2f080a51a10d -r 09ac56914b29 src/Pure/PIDE/protocol.ML --- a/src/Pure/PIDE/protocol.ML Thu May 31 22:10:06 2018 +0200 +++ b/src/Pure/PIDE/protocol.ML Thu May 31 22:27:13 2018 +0200 @@ -64,10 +64,6 @@ end); val _ = - Isabelle_Process.protocol_command "Document.consolidate_execution" - (fn [] => Document.consolidate_execution (Document.state ())); - -val _ = Isabelle_Process.protocol_command "Document.discontinue_execution" (fn [] => Execution.discontinue ()); @@ -78,49 +74,52 @@ val _ = Isabelle_Process.protocol_command "Document.update" (Future.task_context "Document.update" (Future.new_group NONE) - (fn [old_id_string, new_id_string, edits_yxml] => Document.change_state (fn state => - let - val _ = Execution.discontinue (); + (fn [old_id_string, new_id_string, edits_yxml, consolidate_string] => + Document.change_state (fn state => + let + val old_id = Document_ID.parse old_id_string; + val new_id = Document_ID.parse new_id_string; + val edits = + YXML.parse_body edits_yxml |> + let open XML.Decode in + list (pair string + (variant + [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), + fn ([], a) => + let + val (master, (name, (imports, (keywords, errors)))) = + pair string (pair string (pair (list string) + (pair (list (pair string + (pair (pair string (list string)) (list string)))) + (list YXML.string_of_body)))) a; + val imports' = map (rpair Position.none) imports; + val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords; + val header = Thy_Header.make (name, Position.none) imports' keywords'; + in Document.Deps {master = master, header = header, errors = errors} end, + fn (a :: b, c) => + Document.Perspective (bool_atom a, map int_atom b, + list (pair int (pair string (list string))) c)])) + end; + val consolidate = Value.parse_bool consolidate_string; - val old_id = Document_ID.parse old_id_string; - val new_id = Document_ID.parse new_id_string; - val edits = - YXML.parse_body edits_yxml |> - let open XML.Decode in - list (pair string - (variant - [fn ([], a) => Document.Edits (list (pair (option int) (option int)) a), - fn ([], a) => - let - val (master, (name, (imports, (keywords, errors)))) = - pair string (pair string (pair (list string) - (pair (list (pair string - (pair (pair string (list string)) (list string)))) - (list YXML.string_of_body)))) a; - val imports' = map (rpair Position.none) imports; - val keywords' = map (fn (x, y) => ((x, Position.none), y)) keywords; - val header = Thy_Header.make (name, Position.none) imports' keywords'; - in Document.Deps {master = master, header = header, errors = errors} end, - fn (a :: b, c) => - Document.Perspective (bool_atom a, map int_atom b, - list (pair int (pair string (list string))) c)])) - end; + val _ = Execution.discontinue (); - val (removed, assign_update, state') = Document.update old_id new_id edits state; - val _ = - (singleton o Future.forks) - {name = "Document.update/remove", group = NONE, - deps = Execution.snapshot removed, - pri = Task_Queue.urgent_pri + 2, interrupts = false} - (fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed)); + val (removed, assign_update, state') = + Document.update old_id new_id edits consolidate state; + val _ = + (singleton o Future.forks) + {name = "Document.update/remove", group = NONE, + deps = Execution.snapshot removed, + pri = Task_Queue.urgent_pri + 2, interrupts = false} + (fn () => (Execution.purge removed; List.app Isabelle_Process.reset_tracing removed)); - val _ = - Output.protocol_message Markup.assign_update - [(new_id, assign_update) |> - let open XML.Encode - in pair int (list (pair int (list int))) end - |> YXML.string_of_body]; - in Document.start_execution state' end))); + val _ = + Output.protocol_message Markup.assign_update + [(new_id, assign_update) |> + let open XML.Encode + in pair int (list (pair int (list int))) end + |> YXML.string_of_body]; + in Document.start_execution state' end))); val _ = Isabelle_Process.protocol_command "Document.remove_versions" diff -r 2f080a51a10d -r 09ac56914b29 src/Pure/PIDE/protocol.scala --- a/src/Pure/PIDE/protocol.scala Thu May 31 22:10:06 2018 +0200 +++ b/src/Pure/PIDE/protocol.scala Thu May 31 22:27:13 2018 +0200 @@ -409,9 +409,6 @@ /* execution */ - def consolidate_execution(): Unit = - protocol_command("Document.consolidate_execution") - def discontinue_execution(): Unit = protocol_command("Document.discontinue_execution") @@ -422,7 +419,7 @@ /* document versions */ def update(old_id: Document_ID.Version, new_id: Document_ID.Version, - edits: List[Document.Edit_Command]) + edits: List[Document.Edit_Command], consolidate: Boolean) { val edits_yxml = { @@ -450,7 +447,8 @@ pair(string, encode_edit(name))(name.node, edit) }) Symbol.encode_yxml(encode_edits(edits)) } - protocol_command("Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml) + protocol_command( + "Document.update", Document_ID(old_id), Document_ID(new_id), edits_yxml, consolidate.toString) } def remove_versions(versions: List[Document.Version]) diff -r 2f080a51a10d -r 09ac56914b29 src/Pure/PIDE/resources.scala --- a/src/Pure/PIDE/resources.scala Thu May 31 22:10:06 2018 +0200 +++ b/src/Pure/PIDE/resources.scala Thu May 31 22:27:13 2018 +0200 @@ -215,8 +215,9 @@ reparse_limit: Int, previous: Document.Version, doc_blobs: Document.Blobs, - edits: List[Document.Edit_Text]): Session.Change = - Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits) + edits: List[Document.Edit_Text], + consolidate: Boolean): Session.Change = + Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits, consolidate) def commit(change: Session.Change) { } diff -r 2f080a51a10d -r 09ac56914b29 src/Pure/PIDE/session.scala --- a/src/Pure/PIDE/session.scala Thu May 31 22:10:06 2018 +0200 +++ b/src/Pure/PIDE/session.scala Thu May 31 22:27:13 2018 +0200 @@ -50,6 +50,7 @@ syntax_changed: List[Document.Node.Name], deps_changed: Boolean, doc_edits: List[Document.Edit_Command], + consolidate: Boolean, version: Document.Version) case object Change_Flush @@ -230,15 +231,16 @@ previous: Future[Document.Version], doc_blobs: Document.Blobs, text_edits: List[Document.Edit_Text], + consolidate: Boolean, version_result: Promise[Document.Version]) private val change_parser = Consumer_Thread.fork[Text_Edits]("change_parser", daemon = true) { - case Text_Edits(previous, doc_blobs, text_edits, version_result) => + case Text_Edits(previous, doc_blobs, text_edits, consolidate, version_result) => val prev = previous.get_finished val change = Timing.timeit("parse_change", timing) { - resources.parse_change(reparse_limit, prev, doc_blobs, text_edits) + resources.parse_change(reparse_limit, prev, doc_blobs, text_edits, consolidate) } version_result.fulfill(change.version) manager.send(change) @@ -342,7 +344,10 @@ { /* raw edits */ - def handle_raw_edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text]) + def handle_raw_edits( + doc_blobs: Document.Blobs = Document.Blobs.empty, + edits: List[Document.Edit_Text] = Nil, + consolidate: Boolean = false) //{{{ { require(prover.defined) @@ -354,7 +359,7 @@ global_state.change(_.continue_history(previous, edits, version)) raw_edits.post(Session.Raw_Edits(doc_blobs, edits)) - change_parser.send(Text_Edits(previous, doc_blobs, edits, version)) + change_parser.send(Text_Edits(previous, doc_blobs, edits, consolidate, version)) } //}}} @@ -392,7 +397,7 @@ val assignment = global_state.value.the_assignment(change.previous).check_finished global_state.change(_.define_version(change.version, assignment)) - prover.get.update(change.previous.id, change.version.id, change.doc_edits) + prover.get.update(change.previous.id, change.version.id, change.doc_edits, change.consolidate) resources.commit(change) } //}}} @@ -529,7 +534,7 @@ } case Consolidate_Execution => - if (prover.defined) prover.get.consolidate_execution() + if (prover.defined) handle_raw_edits(consolidate = true) case Prune_History => if (prover.defined) { @@ -540,7 +545,7 @@ case Update_Options(options) => if (prover.defined && is_ready) { prover.get.options(options) - handle_raw_edits(Document.Blobs.empty, Nil) + handle_raw_edits() } global_options.post(Session.Global_Options(options)) @@ -548,7 +553,7 @@ prover.get.cancel_exec(exec_id) case Session.Raw_Edits(doc_blobs, edits) if prover.defined => - handle_raw_edits(doc_blobs, edits) + handle_raw_edits(doc_blobs = doc_blobs, edits = edits) case Session.Dialog_Result(id, serial, result) if prover.defined => prover.get.dialog_result(serial, result) diff -r 2f080a51a10d -r 09ac56914b29 src/Pure/Thy/thy_syntax.scala --- a/src/Pure/Thy/thy_syntax.scala Thu May 31 22:10:06 2018 +0200 +++ b/src/Pure/Thy/thy_syntax.scala Thu May 31 22:27:13 2018 +0200 @@ -296,7 +296,8 @@ reparse_limit: Int, previous: Document.Version, doc_blobs: Document.Blobs, - edits: List[Document.Edit_Text]): Session.Change = + edits: List[Document.Edit_Text], + consolidate: Boolean): Session.Change = { val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits) @@ -356,6 +357,7 @@ (doc_edits.toList.filterNot(_._2.is_void), Document.Version.make(nodes)) } - Session.Change(previous, syntax_changed, syntax_changed.nonEmpty, doc_edits, version) + Session.Change( + previous, syntax_changed, syntax_changed.nonEmpty, doc_edits, consolidate, version) } }