# HG changeset patch
# User paulson
# Date 1525300380 -3600
# Node ID 8dc792d440b949a681c460d59130fde073f8e33d
# Parent  0acf3206a723993fac5d9487bcd68f3f45bb06b5# Parent  36209dfb981efedc434fe7b8207345491b939e91
merged

diff -r 36209dfb981e -r 8dc792d440b9 NEWS
--- a/NEWS	Wed May 02 23:32:47 2018 +0100
+++ b/NEWS	Wed May 02 23:33:00 2018 +0100
@@ -110,7 +110,8 @@
 notably bibtex database files and ML files.
 
 * Action "isabelle.draft" is similar to "isabelle.preview", but shows a
-plain-text document draft.
+plain-text document draft. Both are available via the menu "Plugins /
+Isabelle".
 
 * When loading text files, the Isabelle symbols encoding UTF-8-Isabelle
 is only used if there is no conflict with existing Unicode sequences in
diff -r 36209dfb981e -r 8dc792d440b9 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Wed May 02 23:32:47 2018 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Wed May 02 23:33:00 2018 +0100
@@ -73,9 +73,9 @@
   Isabelle/jEdit (\figref{fig:isabelle-jedit}) consists of some plugins for
   the jEdit text editor, while preserving its general look-and-feel as far as
   possible. The main plugin is called ``Isabelle'' and has its own menu
-  \<^emph>\<open>Plugins~/ Isabelle\<close> with access to several panels (see also
-  \secref{sec:dockables}), as well as \<^emph>\<open>Plugins~/ Plugin Options~/ Isabelle\<close>
-  (see also \secref{sec:options}).
+  \<^emph>\<open>Plugins~/ Isabelle\<close> with access to several actions and add-on panels (see
+  also \secref{sec:dockables}), as well as \<^emph>\<open>Plugins~/ Plugin Options~/
+  Isabelle\<close> (see also \secref{sec:options}).
 
   The options allow to specify a logic session name, but the same selector is
   also accessible in the \<^emph>\<open>Theories\<close> panel (\secref{sec:theories}). After
diff -r 36209dfb981e -r 8dc792d440b9 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed May 02 23:32:47 2018 +0100
+++ b/src/Pure/PIDE/document.scala	Wed May 02 23:33:00 2018 +0100
@@ -412,6 +412,19 @@
     def purge(f: Version => Option[Version], versions: Map[Document_ID.Version, Version])
       : Map[Document_ID.Version, Version] =
       (versions /: (for ((id, v) <- versions.iterator; v1 <- f(v)) yield (id, v1)))(_ + _)
+
+    def purge_future(versions: Map[Document_ID.Version, Version], future: Future[Version])
+      : Future[Version] =
+    {
+      if (future.is_finished) {
+        val version = future.join
+        versions.get(version.id) match {
+          case Some(version1) if !(version eq version1) => Future.value(version1)
+          case _ => future
+        }
+      }
+      else future
+    }
   }
 
   final class Version private(
@@ -449,6 +462,14 @@
       version.is_finished
 
     def truncate: Change = new Change(None, Nil, version)
+
+    def purge(versions: Map[Document_ID.Version, Version]): Option[Change] =
+    {
+      val previous1 = previous.map(Version.purge_future(versions, _))
+      val version1 = Version.purge_future(versions, version)
+      if ((previous eq previous1) && (version eq version1)) None
+      else Some(new Change(previous1, rev_edits, version1))
+    }
   }
 
 
@@ -477,6 +498,13 @@
         case _ => None
       }
     }
+
+    def purge(versions: Map[Document_ID.Version, Version]): History =
+    {
+      val undo_list1 = undo_list.map(_.purge(versions))
+      if (undo_list1.forall(_.isEmpty)) this
+      else new History(for ((a, b) <- undo_list1 zip undo_list) yield a.getOrElse(b))
+    }
   }
 
 
@@ -786,13 +814,16 @@
         }
       }
 
+      val versions2 = Version.purge(_.purge_blobs(blobs1_names), versions1)
+
       copy(
-        versions = Version.purge(_.purge_blobs(blobs1_names), versions1),
+        versions = versions2,
         blobs = blobs1,
         commands = commands1,
         execs = execs1,
         commands_redirection = commands_redirection.restrict(commands1.isDefinedAt(_)),
         assignments = assignments1,
+        history = history.purge(versions2),
         removing_versions = false)
     }
 
diff -r 36209dfb981e -r 8dc792d440b9 src/Pure/proofterm.ML
--- a/src/Pure/proofterm.ML	Wed May 02 23:32:47 2018 +0100
+++ b/src/Pure/proofterm.ML	Wed May 02 23:33:00 2018 +0100
@@ -1613,11 +1613,15 @@
     val body0 =
       if not (proofs_enabled ()) then Future.value (make_body0 MinProof)
       else
-        (singleton o Future.cond_forks)
-          {name = "Proofterm.prepare_thm_proof", group = NONE,
-            deps = [], pri = 1, interrupts = true}
-          (fn () =>
-            make_body0 (shrink_proof (rew_proof thy (fold_rev implies_intr_proof hyps prf))));
+        let
+          val rew = rew_proof thy;
+          val prf' = fold_rev implies_intr_proof hyps prf;
+        in
+          (singleton o Future.cond_forks)
+            {name = "Proofterm.prepare_thm_proof", group = NONE,
+              deps = [], pri = 1, interrupts = true}
+            (fn () => make_body0 (shrink_proof (rew prf')))
+        end;
 
     fun new_prf () = (serial (), fulfill_proof_future thy promises postproc body0);
     val (i, body') =
diff -r 36209dfb981e -r 8dc792d440b9 src/Tools/jEdit/src/Isabelle.props
--- a/src/Tools/jEdit/src/Isabelle.props	Wed May 02 23:32:47 2018 +0100
+++ b/src/Tools/jEdit/src/Isabelle.props	Wed May 02 23:33:00 2018 +0100
@@ -30,6 +30,9 @@
 #menu actions and dockables
 plugin.isabelle.jedit.Plugin.menu.label=Isabelle
 plugin.isabelle.jedit.Plugin.menu= \
+  isabelle.preview \
+  isabelle.draft \
+  - \
   isabelle-debugger \
   isabelle-documentation \
   isabelle-monitor \
diff -r 36209dfb981e -r 8dc792d440b9 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Wed May 02 23:32:47 2018 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Wed May 02 23:33:00 2018 +0100
@@ -215,6 +215,7 @@
 isabelle.decrease-font-size.shortcut2=C+SUBTRACT
 isabelle.decrease-font-size.shortcut=C+MINUS
 isabelle.decrease-font-size2.label=Decrease font size (clone)
+isabelle.draft.label=Show draft in browser
 isabelle.exclude-word-permanently.label=Exclude word permanently
 isabelle.exclude-word.label=Exclude word
 isabelle.include-word-permanently.label=Include word permanently
@@ -227,7 +228,7 @@
 isabelle.newline.label=Newline with indentation of Isabelle keywords
 isabelle.newline.shortcut=ENTER
 isabelle.options.label=Isabelle options
-isabelle.preview.label=HTML preview of PIDE document
+isabelle.preview.label=Show preview in browser
 isabelle.reset-continuous-checking.label=Reset continuous checking
 isabelle.reset-font-size.label=Reset font size
 isabelle.reset-node-required.label=Reset node required