--- a/NEWS Sun Aug 20 03:35:20 2017 +0200
+++ b/NEWS Sun Aug 20 21:37:55 2017 +0200
@@ -105,6 +105,10 @@
painted with thick lines; remaining errors in this situation are
represented by a different border color.
+* The main Isabelle/jEdit plugin may be restarted manually (using the
+jEdit Plugin Manager), as long as the "Isabelle Base" plugin remains
+enabled at all times.
+
* Update to jedit-5.4.0.
--- a/src/Doc/JEdit/JEdit.thy Sun Aug 20 03:35:20 2017 +0200
+++ b/src/Doc/JEdit/JEdit.thy Sun Aug 20 21:37:55 2017 +0200
@@ -144,17 +144,16 @@
sense how it is meant to work, before loading too many other plugins.
\<^medskip>
- The main \<^emph>\<open>Isabelle\<close> plugin is an integral part of Isabelle/jEdit and needs
- to remain active at all times! A few additional plugins are bundled with
- Isabelle/jEdit for convenience or out of necessity, notably \<^emph>\<open>Console\<close> with
- its Isabelle/Scala sub-plugin (\secref{sec:scala-console}) and \<^emph>\<open>SideKick\<close>
- with some Isabelle-specific parsers for document tree structure
- (\secref{sec:sidekick}). The \<^emph>\<open>Navigator\<close> plugin is particularly important
- for hyperlinks within the formal document-model
- (\secref{sec:tooltips-hyperlinks}). Further plugins (e.g.\ \<^emph>\<open>ErrorList\<close>,
- \<^emph>\<open>Code2HTML\<close>) are included to saturate the dependencies of bundled plugins,
- but have no particular use in Isabelle/jEdit.
-\<close>
+ The \<^emph>\<open>Isabelle\<close> plugin provides the main Prover IDE functionality of
+ Isabelle/jEdit: it manages the prover session in the background. A few
+ additional plugins are bundled with Isabelle/jEdit for convenience or out of
+ necessity, notably \<^emph>\<open>Console\<close> with its Isabelle/Scala sub-plugin
+ (\secref{sec:scala-console}) and \<^emph>\<open>SideKick\<close> with some Isabelle-specific
+ parsers for document tree structure (\secref{sec:sidekick}). The
+ \<^emph>\<open>Navigator\<close> plugin is particularly important for hyperlinks within the
+ formal document-model (\secref{sec:tooltips-hyperlinks}). Further plugins
+ (e.g.\ \<^emph>\<open>ErrorList\<close>, \<^emph>\<open>Code2HTML\<close>) are included to saturate the dependencies
+ of bundled plugins, but have no particular use in Isabelle/jEdit. \<close>
subsection \<open>Options \label{sec:options}\<close>
@@ -497,13 +496,14 @@
paragraph \<open>Encoding.\<close>
text \<open>Technically, the Unicode interpretation of Isabelle symbols is an
\<^emph>\<open>encoding\<close> called \<^verbatim>\<open>UTF-8-Isabelle\<close> in jEdit (\<^emph>\<open>not\<close> in the underlying
- JVM). It is provided by the Isabelle/jEdit plugin and enabled by default for
- all source files. Sometimes such defaults are reset accidentally, or
- malformed UTF-8 sequences in the text force jEdit to fall back on a
- different encoding like \<^verbatim>\<open>ISO-8859-15\<close>. In that case, verbatim ``\<^verbatim>\<open>\<alpha>\<close>'' will
- be shown in the text buffer instead of its Unicode rendering ``\<open>\<alpha>\<close>''. The
- jEdit menu operation \<^emph>\<open>File~/ Reload with Encoding~/ UTF-8-Isabelle\<close> helps
- to resolve such problems (after repairing malformed parts of the text). \<close>
+ JVM). It is provided by the Isabelle Base plugin and enabled by default for
+ all source files in Isabelle/jEdit. Sometimes such defaults are reset
+ accidentally, or malformed UTF-8 sequences in the text force jEdit to fall
+ back on a different encoding like \<^verbatim>\<open>ISO-8859-15\<close>. In that case, verbatim
+ ``\<^verbatim>\<open>\<alpha>\<close>'' will be shown in the text buffer instead of its Unicode rendering
+ ``\<open>\<alpha>\<close>''. The jEdit menu operation \<^emph>\<open>File~/ Reload with Encoding~/
+ UTF-8-Isabelle\<close> helps to resolve such problems (after repairing malformed
+ parts of the text). \<close>
paragraph \<open>Font.\<close>
text \<open>Correct rendering via Unicode requires a font that contains glyphs for
--- a/src/Pure/Tools/main.scala Sun Aug 20 03:35:20 2017 +0200
+++ b/src/Pure/Tools/main.scala Sun Aug 20 21:37:55 2017 +0200
@@ -26,6 +26,14 @@
/* settings directory */
val settings_dir = Path.explode("$JEDIT_SETTINGS")
+
+ val properties = settings_dir + Path.explode("properties")
+ if (properties.is_file) {
+ val props1 = split_lines(File.read(properties))
+ val props2 = props1.filterNot(_.startsWith("plugin-blacklist.Isabelle-jEdit"))
+ if (props1 != props2) File.write(properties, cat_lines(props2))
+ }
+
Isabelle_System.mkdirs(settings_dir + Path.explode("DockableWindowManager"))
if (!(settings_dir + Path.explode("perspective.xml")).is_file) {
--- a/src/Pure/Tools/simplifier_trace.scala Sun Aug 20 03:35:20 2017 +0200
+++ b/src/Pure/Tools/simplifier_trace.scala Sun Aug 20 21:37:55 2017 +0200
@@ -140,7 +140,7 @@
def send_reply(session: Session, serial: Long, answer: Answer) =
manager.send(Reply(session, serial, answer))
- private lazy val manager: Consumer_Thread[Any] =
+ def make_manager: Consumer_Thread[Any] =
{
var contexts = Map.empty[Document_ID.Command, Context]
@@ -283,17 +283,27 @@
)
}
+ private val manager_variable = Synchronized[Option[Consumer_Thread[Any]]](None)
+
+ def manager: Consumer_Thread[Any] =
+ manager_variable.value match {
+ case Some(thread) if thread.is_active => thread
+ case _ => error("Bad Simplifier_Trace.manager thread")
+ }
+
/* protocol handler */
class Handler extends Session.Protocol_Handler
{
- assert(manager.is_active)
+ try { manager }
+ catch { case ERROR(_) => manager_variable.change(_ => Some(make_manager)) }
override def exit() =
{
manager.send(Clear_Memory)
manager.shutdown()
+ manager_variable.change(_ => None)
}
private def cancel(msg: Prover.Protocol_Output): Boolean =
--- a/src/Tools/jEdit/lib/Tools/jedit Sun Aug 20 03:35:20 2017 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Sun Aug 20 21:37:55 2017 +0200
@@ -19,6 +19,16 @@
## sources
+declare -a SOURCES_BASE=(
+ "src-base/isabelle_encoding.scala"
+ "src-base/plugin.scala"
+)
+
+declare -a RESOURCES_BASE=(
+ "src-base/Isabelle_Base.props"
+ "src-base/services.xml"
+)
+
declare -a SOURCES=(
"src/active.scala"
"src/completion_popup.scala"
@@ -248,6 +258,7 @@
# target
+TARGET_BASE="dist/jars/Isabelle-jEdit-base.jar"
TARGET="dist/jars/Isabelle-jEdit.jar"
declare -a UPDATED=()
@@ -256,23 +267,28 @@
OUTDATED=true
else
OUTDATED=false
- if [ ! -e "$TARGET" ]; then
+ if [ ! -e "$TARGET_BASE" -a ! -e "$TARGET" ]; then
OUTDATED=true
else
if [ -n "$ISABELLE_JEDIT_BUILD_HOME" ]; then
declare -a DEPS=(
"$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR"
+ "${SOURCES_BASE[@]}" "${RESOURCES_BASE[@]}"
"${SOURCES[@]}" "${RESOURCES[@]}"
)
elif [ -e "$ISABELLE_HOME/Admin/build" ]; then
- declare -a DEPS=("$PURE_JAR" "${SOURCES[@]}" "${RESOURCES[@]}")
+ declare -a DEPS=(
+ "$PURE_JAR"
+ "${SOURCES_BASE[@]}" "${RESOURCES_BASE[@]}"
+ "${SOURCES[@]}" "${RESOURCES[@]}"
+ )
else
declare -a DEPS=()
fi
for DEP in "${DEPS[@]}"
do
[ ! -e "$DEP" ] && fail "Missing file: $DEP"
- [ "$DEP" -nt "$TARGET" ] && {
+ [ "$DEP" -nt "$TARGET_BASE" -o "$DEP" -nt "$TARGET" ] && {
OUTDATED=true
UPDATED["${#UPDATED[@]}"]="$DEP"
}
@@ -283,6 +299,37 @@
# build
+function init_resources ()
+{
+ mkdir -p dist/classes || failed
+ cp -p -R -f "$@" dist/classes/.
+}
+
+function compile_sources ()
+{
+ (
+ #FIXME workarounds for scalac 2.11.0
+ export CYGWIN="nodosfilewarning"
+ function stty() { :; }
+ export -f stty
+
+ for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR"
+ do
+ classpath "$JAR"
+ done
+ export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")"
+ isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d dist/classes "$@"
+ ) || fail "Failed to compile sources"
+}
+
+function make_jar ()
+{
+ cd dist/classes
+ isabelle_jdk jar cf "../../$1" * || failed
+ cd ../..
+ rm -rf dist/classes
+}
+
if [ "$OUTDATED" = true ]
then
echo "### Building Isabelle/jEdit ..."
@@ -299,10 +346,15 @@
fail "Unknown ISABELLE_JEDIT_BUILD_HOME -- missing auxiliary component"
rm -rf dist || failed
- mkdir -p dist dist/classes || failed
+ mkdir -p dist || failed
cp -p -R -f "$ISABELLE_JEDIT_BUILD_HOME/contrib/$ISABELLE_JEDIT_BUILD_VERSION/." dist/.
- cp -p -R -f "${RESOURCES[@]}" dist/classes/.
+
+ init_resources "${RESOURCES_BASE[@]}"
+ compile_sources "${SOURCES_BASE[@]}"
+ make_jar "$TARGET_BASE"
+
+ init_resources "${RESOURCES[@]}"
cp src/jEdit.props dist/properties/.
cp -p -R -f src/modes/. dist/modes/.
@@ -334,24 +386,8 @@
cd ..
cp -p -R -f "${JEDIT_JARS[@]}" dist/jars/. || failed
- (
- #FIXME workarounds for scalac 2.11.0
- export CYGWIN="nodosfilewarning"
- function stty() { :; }
- export -f stty
-
- for JAR in "$JEDIT_JAR" "${JEDIT_JARS[@]}" "$PURE_JAR"
- do
- classpath "$JAR"
- done
- export CLASSPATH="$(platform_path "$ISABELLE_CLASSPATH")"
- isabelle_scala scalac $ISABELLE_SCALAC_OPTIONS -d dist/classes "${SOURCES[@]}"
- ) || fail "Failed to compile sources"
-
- cd dist/classes
- isabelle_jdk jar cf "../jars/Isabelle-jEdit.jar" * || failed
- cd ../..
- rm -rf dist/classes
+ compile_sources "${SOURCES[@]}"
+ make_jar "$TARGET"
cp "$ISABELLE_JEDIT_BUILD_HOME/doc/jedit5.4.0manual-a4.pdf" dist/doc/jedit-manual.pdf
cp dist/doc/CHANGES.txt dist/doc/jedit-changes
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src-base/isabelle_encoding.scala Sun Aug 20 21:37:55 2017 +0200
@@ -0,0 +1,54 @@
+/* Title: Tools/jEdit/src-base/isabelle_encoding.scala
+ Author: Makarius
+
+Isabelle encoding -- based on UTF-8.
+*/
+
+package isabelle.jedit_base
+
+
+import isabelle._
+
+import org.gjt.sp.jedit.io.Encoding
+
+import java.nio.charset.{Charset, CodingErrorAction}
+import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
+ CharArrayReader, ByteArrayOutputStream}
+
+import scala.io.{Codec, BufferedSource}
+
+
+class Isabelle_Encoding extends Encoding
+{
+ private val BUFSIZE = 32768
+
+ private def text_reader(in: InputStream, codec: Codec): Reader =
+ {
+ val source = new BufferedSource(in)(codec)
+ new CharArrayReader(Symbol.decode(source.mkString).toArray)
+ }
+
+ override def getTextReader(in: InputStream): Reader = text_reader(in, UTF8.codec())
+
+ override def getPermissiveTextReader(in: InputStream): Reader =
+ {
+ val codec = UTF8.codec()
+ codec.onMalformedInput(CodingErrorAction.REPLACE)
+ codec.onUnmappableCharacter(CodingErrorAction.REPLACE)
+ text_reader(in, codec)
+ }
+
+ override def getTextWriter(out: OutputStream): Writer =
+ {
+ val buffer = new ByteArrayOutputStream(BUFSIZE) {
+ override def flush()
+ {
+ val text = Symbol.encode(toString(UTF8.charset_name))
+ out.write(UTF8.bytes(text))
+ out.flush()
+ }
+ override def close() { out.close() }
+ }
+ new OutputStreamWriter(buffer, UTF8.charset.newEncoder())
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src-base/plugin.scala Sun Aug 20 21:37:55 2017 +0200
@@ -0,0 +1,21 @@
+/* Title: Tools/jEdit/src-base/plugin.scala
+ Author: Makarius
+
+Isabelle base environment for jEdit.
+*/
+
+package isabelle.jedit_base
+
+
+import isabelle._
+
+import org.gjt.sp.jedit.EBPlugin
+
+
+class Plugin extends EBPlugin
+{
+ override def start()
+ {
+ Isabelle_System.init()
+ }
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src-base/services.xml Sun Aug 20 21:37:55 2017 +0200
@@ -0,0 +1,8 @@
+<?xml version="1.0"?>
+<!DOCTYPE SERVICES SYSTEM "services.dtd">
+
+<SERVICES>
+ <SERVICE NAME="UTF-8-Isabelle" CLASS="org.gjt.sp.jedit.io.Encoding">
+ new isabelle.jedit_base.Isabelle_Encoding();
+ </SERVICE>
+</SERVICES>
--- a/src/Tools/jEdit/src/Isabelle.props Sun Aug 20 03:35:20 2017 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props Sun Aug 20 21:37:55 2017 +0200
@@ -5,11 +5,11 @@
#identification
plugin.isabelle.jedit.Plugin.name=Isabelle
plugin.isabelle.jedit.Plugin.author=Johannes Hölzl, Lars Hupel, Fabian Immler, Markus Kaiser, Makarius Wenzel
-plugin.isabelle.jedit.Plugin.version=8.0
+plugin.isabelle.jedit.Plugin.version=9.0
plugin.isabelle.jedit.Plugin.description=Isabelle Prover IDE
#system parameters
-plugin.isabelle.jedit.Plugin.activate=startup
+plugin.isabelle.jedit.Plugin.activate=defer
plugin.isabelle.jedit.Plugin.usePluginHome=false
#dependencies
@@ -18,6 +18,7 @@
plugin.isabelle.jedit.Plugin.depend.2=plugin console.ConsolePlugin 5.1.4
plugin.isabelle.jedit.Plugin.depend.3=plugin errorlist.ErrorListPlugin 2.3
plugin.isabelle.jedit.Plugin.depend.4=plugin sidekick.SideKickPlugin 1.8
+plugin.isabelle.jedit.Plugin.depend.5=plugin isabelle.jedit_base.Plugin 1.0
#options
plugin.isabelle.jedit.Plugin.option-group=isabelle-general isabelle-rendering
--- a/src/Tools/jEdit/src/isabelle_encoding.scala Sun Aug 20 03:35:20 2017 +0200
+++ b/src/Tools/jEdit/src/isabelle_encoding.scala Sun Aug 20 21:37:55 2017 +0200
@@ -9,58 +9,14 @@
import isabelle._
-import org.gjt.sp.jedit.io.Encoding
import org.gjt.sp.jedit.buffer.JEditBuffer
-import java.nio.charset.{Charset, CodingErrorAction}
-import java.io.{InputStream, OutputStream, Reader, Writer, InputStreamReader, OutputStreamWriter,
- CharArrayReader, ByteArrayOutputStream}
-
-import scala.io.{Codec, BufferedSource}
-
object Isabelle_Encoding
{
- val NAME = "UTF-8-Isabelle"
-
def is_active(buffer: JEditBuffer): Boolean =
- buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == NAME
+ buffer.getStringProperty(JEditBuffer.ENCODING).asInstanceOf[String] == "UTF-8-Isabelle"
def maybe_decode(buffer: JEditBuffer, s: String): String =
if (is_active(buffer)) Symbol.decode(s) else s
}
-
-class Isabelle_Encoding extends Encoding
-{
- private val BUFSIZE = 32768
-
- private def text_reader(in: InputStream, codec: Codec): Reader =
- {
- val source = new BufferedSource(in)(codec)
- new CharArrayReader(Symbol.decode(source.mkString).toArray)
- }
-
- override def getTextReader(in: InputStream): Reader = text_reader(in, UTF8.codec())
-
- override def getPermissiveTextReader(in: InputStream): Reader =
- {
- val codec = UTF8.codec()
- codec.onMalformedInput(CodingErrorAction.REPLACE)
- codec.onUnmappableCharacter(CodingErrorAction.REPLACE)
- text_reader(in, codec)
- }
-
- override def getTextWriter(out: OutputStream): Writer =
- {
- val buffer = new ByteArrayOutputStream(BUFSIZE) {
- override def flush()
- {
- val text = Symbol.encode(toString(UTF8.charset_name))
- out.write(UTF8.bytes(text))
- out.flush()
- }
- override def close() { out.close() }
- }
- new OutputStreamWriter(buffer, UTF8.charset.newEncoder())
- }
-}
--- a/src/Tools/jEdit/src/isabelle_options.scala Sun Aug 20 03:35:20 2017 +0200
+++ b/src/Tools/jEdit/src/isabelle_options.scala Sun Aug 20 21:37:55 2017 +0200
@@ -42,7 +42,7 @@
val options = PIDE.options
private val predefined =
- List(JEdit_Sessions.logic_selector(options.value, false),
+ List(JEdit_Sessions.logic_selector(options, false),
JEdit_Spell_Checker.dictionaries_selector())
protected val components =
--- a/src/Tools/jEdit/src/jedit_editor.scala Sun Aug 20 03:35:20 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_editor.scala Sun Aug 20 21:37:55 2017 +0200
@@ -39,6 +39,13 @@
def invoke(): Unit = delay1_flush.invoke()
def invoke_generated(): Unit = { delay1_flush.invoke(); delay2_flush.invoke() }
+ def shutdown(): Unit =
+ GUI_Thread.require {
+ delay1_flush.revoke()
+ delay2_flush.revoke()
+ Document_Model.flush_edits(hidden = false, purge = false)
+ }
+
def visible_node(name: Document.Node.Name): Boolean =
(for {
text_area <- JEdit_Lib.jedit_text_areas()
--- a/src/Tools/jEdit/src/jedit_sessions.scala Sun Aug 20 03:35:20 2017 +0200
+++ b/src/Tools/jEdit/src/jedit_sessions.scala Sun Aug 20 21:37:55 2017 +0200
@@ -100,13 +100,13 @@
override def toString: String = description
}
- def logic_selector(options: Options, autosave: Boolean): Option_Component =
+ def logic_selector(options: Options_Variable, autosave: Boolean): Option_Component =
{
GUI_Thread.require {}
val entries =
- new Logic_Entry("", "default (" + session_name(options) + ")") ::
- session_list(options).map(name => new Logic_Entry(name, name))
+ new Logic_Entry("", "default (" + session_name(options.value) + ")") ::
+ session_list(options.value).map(name => new Logic_Entry(name, name))
val component = new ComboBox(entries) with Option_Component {
name = option_name
--- a/src/Tools/jEdit/src/plugin.scala Sun Aug 20 03:35:20 2017 +0200
+++ b/src/Tools/jEdit/src/plugin.scala Sun Aug 20 21:37:55 2017 +0200
@@ -211,7 +211,7 @@
GUI_Thread.later {
delay_load.revoke()
delay_init.revoke()
- PIDE.editor.flush()
+ PIDE.editor.shutdown()
exit_models(JEdit_Lib.jedit_buffers().toList)
}
@@ -281,6 +281,12 @@
@volatile private var startup_failure: Option[Throwable] = None
@volatile private var startup_notified = false
+ private def init_view(view: View)
+ {
+ Session_Build.check_dialog(view)
+ Keymap_Merge.check_dialog(view)
+ }
+
override def handleMessage(message: EBMessage)
{
GUI_Thread.assert {}
@@ -306,10 +312,7 @@
}
val view = jEdit.getActiveView()
-
- Session_Build.check_dialog(view)
-
- Keymap_Merge.check_dialog(view)
+ init_view(view)
PIDE.editor.hyperlink_position(true, Document.Snapshot.init,
JEdit_Sessions.session_info(options.value).open_root).foreach(_.follow(view))
@@ -437,6 +440,9 @@
startup_notified = false
Log.log(Log.ERROR, this, exn)
}
+
+ val view = jEdit.getActiveView()
+ if (view != null) init_view(view)
}
override def stop()
@@ -454,5 +460,6 @@
exit_models(JEdit_Lib.jedit_buffers().toList)
session.stop()
file_watcher.shutdown()
+ PIDE.editor.shutdown()
}
}
--- a/src/Tools/jEdit/src/services.xml Sun Aug 20 03:35:20 2017 +0200
+++ b/src/Tools/jEdit/src/services.xml Sun Aug 20 21:37:55 2017 +0200
@@ -11,9 +11,6 @@
<SERVICE CLASS="org.gjt.sp.jedit.gui.DockingFrameworkProvider" NAME="PIDE">
new isabelle.jedit.PIDE_Docking_Framework();
</SERVICE>
- <SERVICE NAME="UTF-8-Isabelle" CLASS="org.gjt.sp.jedit.io.Encoding">
- new isabelle.jedit.Isabelle_Encoding();
- </SERVICE>
<SERVICE NAME="isabelle" CLASS="sidekick.SideKickParser">
new isabelle.jedit.Isabelle_Sidekick_Default();
</SERVICE>
--- a/src/Tools/jEdit/src/theories_dockable.scala Sun Aug 20 03:35:20 2017 +0200
+++ b/src/Tools/jEdit/src/theories_dockable.scala Sun Aug 20 21:37:55 2017 +0200
@@ -86,7 +86,7 @@
private val continuous_checking = new Isabelle.Continuous_Checking
continuous_checking.focusable = false
- private val logic = JEdit_Sessions.logic_selector(PIDE.options.value, true)
+ private val logic = JEdit_Sessions.logic_selector(PIDE.options, true)
private val controls =
Wrap_Panel(List(purge, continuous_checking, session_phase, logic))