support for share_common_data after define_command and before actual update: this affects string particles of command tokens;

--- a/src/Pure/PIDE/headless.scala	Wed Aug 28 10:18:50 2019 +0200
+++ b/src/Pure/PIDE/headless.scala	Wed Aug 28 22:59:49 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 10:18:50 2019 +0200
+++ b/src/Pure/PIDE/resources.scala	Wed Aug 28 22:59:49 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 10:18:50 2019 +0200
+++ b/src/Pure/PIDE/session.scala	Wed Aug 28 22:59:49 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 10:18:50 2019 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Aug 28 22:59:49 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)
   }
 }