--- a/src/Pure/PIDE/headless.scala Wed Aug 28 19:19:17 2019 +0200
+++ b/src/Pure/PIDE/headless.scala Wed Aug 28 23:19:43 2019 +0200
@@ -158,6 +158,7 @@
watchdog_timeout: Time = default_watchdog_timeout,
nodes_status_delay: Time = default_nodes_status_delay,
id: UUID.T = UUID.random(),
+ share_common_data: Boolean = false,
// commit: must not block, must not fail
commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit] = None,
commit_cleanup_delay: Time = default_commit_cleanup_delay,
@@ -264,7 +265,8 @@
try {
session.commands_changed += consumer
- resources.load_theories(session, id, dep_theories, dep_files, unicode_symbols, progress)
+ resources.load_theories(
+ session, id, dep_theories, dep_files, unicode_symbols, share_common_data, progress)
use_theories_state.value.await_result
check_progress.cancel
}
@@ -537,6 +539,7 @@
dep_theories: List[Document.Node.Name],
dep_files: List[Document.Node.Name],
unicode_symbols: Boolean,
+ share_common_data: Boolean,
progress: Progress)
{
val loaded_theories =
@@ -570,7 +573,8 @@
for { node_name <- dep_files if doc_blobs1.changed(node_name) }
yield st1.blob_edits(node_name, st.blobs.get(node_name))
- session.update(doc_blobs1, theory_edits.flatMap(_._1) ::: file_edits.flatten)
+ session.update(doc_blobs1, theory_edits.flatMap(_._1) ::: file_edits.flatten,
+ share_common_data = share_common_data)
st1.update_theories(theory_edits.map(_._2))
})
}
--- a/src/Pure/PIDE/resources.scala Wed Aug 28 19:19:17 2019 +0200
+++ b/src/Pure/PIDE/resources.scala Wed Aug 28 23:19:43 2019 +0200
@@ -228,8 +228,10 @@
previous: Document.Version,
doc_blobs: Document.Blobs,
edits: List[Document.Edit_Text],
- consolidate: List[Document.Node.Name]): Session.Change =
- Thy_Syntax.parse_change(resources, reparse_limit, previous, doc_blobs, edits, consolidate)
+ consolidate: List[Document.Node.Name],
+ share_common_data: Boolean): Session.Change =
+ Thy_Syntax.parse_change(
+ resources, reparse_limit, previous, doc_blobs, edits, consolidate, share_common_data)
def commit(change: Session.Change) { }
--- a/src/Pure/PIDE/session.scala Wed Aug 28 19:19:17 2019 +0200
+++ b/src/Pure/PIDE/session.scala Wed Aug 28 23:19:43 2019 +0200
@@ -52,6 +52,7 @@
deps_changed: Boolean,
doc_edits: List[Document.Edit_Command],
consolidate: List[Document.Node.Name],
+ share_common_data: Boolean,
version: Document.Version)
case object Change_Flush
@@ -63,7 +64,8 @@
case class Statistics(props: Properties.T)
case class Global_Options(options: Options)
case object Caret_Focus
- case class Raw_Edits(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
+ case class Raw_Edits(
+ doc_blobs: Document.Blobs, edits: List[Document.Edit_Text], share_common_data: Boolean)
case class Dialog_Result(id: Document_ID.Generic, serial: Long, result: String)
case class Build_Theories(id: String, master_dir: Path, theories: List[(Options, List[Path])])
case class Commands_Changed(
@@ -235,15 +237,17 @@
doc_blobs: Document.Blobs,
text_edits: List[Document.Edit_Text],
consolidate: List[Document.Node.Name],
+ share_common_data: 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, consolidate, version_result) =>
+ case Text_Edits(previous, doc_blobs, text_edits, consolidate, share_common_data, version_result) =>
val prev = previous.get_finished
val change =
Timing.timeit("parse_change", timing) {
- resources.parse_change(reparse_limit, prev, doc_blobs, text_edits, consolidate)
+ resources.parse_change(
+ reparse_limit, prev, doc_blobs, text_edits, consolidate, share_common_data)
}
version_result.fulfill(change.version)
manager.send(change)
@@ -390,7 +394,8 @@
def handle_raw_edits(
doc_blobs: Document.Blobs = Document.Blobs.empty,
edits: List[Document.Edit_Text] = Nil,
- consolidate: List[Document.Node.Name] = Nil)
+ consolidate: List[Document.Node.Name] = Nil,
+ share_common_data: Boolean = false)
//{{{
{
require(prover.defined)
@@ -401,8 +406,9 @@
val version = Future.promise[Document.Version]
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, consolidate, version))
+ raw_edits.post(Session.Raw_Edits(doc_blobs, edits, share_common_data))
+ change_parser.send(
+ Text_Edits(previous, doc_blobs, edits, consolidate, share_common_data, version))
}
//}}}
@@ -440,6 +446,10 @@
val assignment = global_state.value.the_assignment(change.previous).check_finished
global_state.change(_.define_version(change.version, assignment))
+
+ if (change.share_common_data) {
+ prover.get.protocol_command("ML_Heap.share_common_data")
+ }
prover.get.update(change.previous.id, change.version.id, change.doc_edits, change.consolidate)
resources.commit(change)
}
@@ -610,8 +620,9 @@
case Cancel_Exec(exec_id) if prover.defined =>
prover.get.cancel_exec(exec_id)
- case Session.Raw_Edits(doc_blobs, edits) if prover.defined =>
- handle_raw_edits(doc_blobs = doc_blobs, edits = edits)
+ case Session.Raw_Edits(doc_blobs, edits, share_common_data) if prover.defined =>
+ handle_raw_edits(doc_blobs = doc_blobs, edits = edits,
+ share_common_data = share_common_data)
case Session.Dialog_Result(id, serial, result) if prover.defined =>
prover.get.dialog_result(serial, result)
@@ -703,8 +714,13 @@
def cancel_exec(exec_id: Document_ID.Exec)
{ manager.send(Cancel_Exec(exec_id)) }
- def update(doc_blobs: Document.Blobs, edits: List[Document.Edit_Text])
- { if (edits.nonEmpty) manager.send_wait(Session.Raw_Edits(doc_blobs, edits)) }
+ def update(
+ doc_blobs: Document.Blobs,
+ edits: List[Document.Edit_Text],
+ share_common_data: Boolean = false)
+ {
+ if (edits.nonEmpty) manager.send_wait(Session.Raw_Edits(doc_blobs, edits, share_common_data))
+ }
def update_options(options: Options)
{ manager.send_wait(Update_Options(options)) }
--- a/src/Pure/Thy/thy_syntax.scala Wed Aug 28 19:19:17 2019 +0200
+++ b/src/Pure/Thy/thy_syntax.scala Wed Aug 28 23:19:43 2019 +0200
@@ -297,7 +297,8 @@
previous: Document.Version,
doc_blobs: Document.Blobs,
edits: List[Document.Edit_Text],
- consolidate: List[Document.Node.Name]): Session.Change =
+ consolidate: List[Document.Node.Name],
+ share_common_data: Boolean): Session.Change =
{
val (syntax_changed, nodes0, doc_edits0) = header_edits(resources, previous, edits)
@@ -358,6 +359,7 @@
}
Session.Change(
- previous, syntax_changed, syntax_changed.nonEmpty, doc_edits, consolidate, version)
+ previous, syntax_changed, syntax_changed.nonEmpty, doc_edits,
+ consolidate, share_common_data, version)
}
}
--- a/src/Pure/Tools/dump.scala Wed Aug 28 19:19:17 2019 +0200
+++ b/src/Pure/Tools/dump.scala Wed Aug 28 23:19:43 2019 +0200
@@ -171,6 +171,7 @@
val use_theories_result =
session.use_theories(use_theories,
unicode_symbols = unicode_symbols,
+ share_common_data = true,
progress = progress,
commit = Some(Consumer.apply _))
@@ -203,8 +204,13 @@
{
val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options
val options1 =
- options0 + "completion_limit=0" + "ML_statistics=false" +
- "parallel_proofs=0" + "editor_tracing_messages=0" + "editor_presentation"
+ options0 +
+ "completion_limit=0" +
+ "ML_statistics=false" +
+ "parallel_proofs=0" +
+ "editor_tracing_messages=0" +
+ "editor_presentation" +
+ "execution_eager"
(options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) })
}