merged
authorpaulson
Thu, 21 Jun 2018 23:06:12 +0100
changeset 68479 f839ce4af873
parent 68477 f090b313fdc8 (diff)
parent 68478 f75a7d2be8c5 (current diff)
child 68485 28f9e9b80c49
merged
--- a/src/Doc/System/Environment.thy	Thu Jun 21 23:05:32 2018 +0100
+++ b/src/Doc/System/Environment.thy	Thu Jun 21 23:06:12 2018 +0100
@@ -205,6 +205,11 @@
   \<^descr>[@{setting_def ISABELLE_TMP_PREFIX}\<open>\<^sup>*\<close>] is the prefix from which any
   running Isabelle ML process derives an individual directory for temporary
   files.
+
+  \<^descr>[@{setting_def ISABELLE_TOOL_JAVA_OPTIONS}] is passed to the \<^verbatim>\<open>java\<close>
+  executable when running Isabelle tools (e.g. @{tool build}). This is
+  occasionally helpful to provide more heap space, via additional options like
+  \<^verbatim>\<open>-Xms1g -Xmx4g\<close>.
 \<close>
 
 
--- a/src/Tools/jEdit/src/document_model.scala	Thu Jun 21 23:05:32 2018 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Jun 21 23:06:12 2018 +0100
@@ -36,6 +36,13 @@
         if model.isInstanceOf[File_Model]
       } yield (node_name, model.asInstanceOf[File_Model])
 
+    def document_blobs: Document.Blobs =
+      Document.Blobs(
+        (for {
+          (node_name, model) <- models.iterator
+          blob <- model.get_blob
+        } yield (node_name -> blob)).toMap)
+
     def open_buffer(session: Session, node_name: Document.Node.Name, buffer: Buffer)
       : (Buffer_Model, State) =
     {
@@ -77,6 +84,8 @@
   def get(name: Document.Node.Name): Option[Document_Model] = get_models.get(name)
   def get(buffer: JEditBuffer): Option[Buffer_Model] = state.value.buffer_models.get(buffer)
 
+  def document_blobs(): Document.Blobs = state.value.document_blobs
+
 
   /* bibtex */
 
@@ -218,12 +227,7 @@
 
     state.change_result(st =>
       {
-        val doc_blobs =
-          Document.Blobs(
-            (for {
-              (node_name, model) <- st.models.iterator
-              blob <- model.get_blob
-            } yield (node_name -> blob)).toMap)
+        val doc_blobs = st.document_blobs
 
         val buffer_edits =
           (for {