--- 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
--- 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
--- 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)
}
--- 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') =
--- 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 \
--- 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