# HG changeset patch # User Manuel Eberl # Date 1503265277 -7200 # Node ID 65ad7a7a9d6a765d1f333119bc8702fbe3be905a # Parent aec5d9c88d69231a325312299e5acf477bc161bc# Parent 86223a532d8e429ea8e6705e8d0c38a32e6dd27e Merged diff -r aec5d9c88d69 -r 65ad7a7a9d6a NEWS --- a/NEWS Sun Aug 20 18:55:03 2017 +0200 +++ b/NEWS Sun Aug 20 23:41:17 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. diff -r aec5d9c88d69 -r 65ad7a7a9d6a src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Sun Aug 20 18:55:03 2017 +0200 +++ b/src/Doc/JEdit/JEdit.thy Sun Aug 20 23:41:17 2017 +0200 @@ -144,17 +144,16 @@ sense how it is meant to work, before loading too many other plugins. \<^medskip> - The main \<^emph>\Isabelle\ 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>\Console\ with - its Isabelle/Scala sub-plugin (\secref{sec:scala-console}) and \<^emph>\SideKick\ - with some Isabelle-specific parsers for document tree structure - (\secref{sec:sidekick}). The \<^emph>\Navigator\ plugin is particularly important - for hyperlinks within the formal document-model - (\secref{sec:tooltips-hyperlinks}). Further plugins (e.g.\ \<^emph>\ErrorList\, - \<^emph>\Code2HTML\) are included to saturate the dependencies of bundled plugins, - but have no particular use in Isabelle/jEdit. -\ + The \<^emph>\Isabelle\ 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>\Console\ with its Isabelle/Scala sub-plugin + (\secref{sec:scala-console}) and \<^emph>\SideKick\ with some Isabelle-specific + parsers for document tree structure (\secref{sec:sidekick}). The + \<^emph>\Navigator\ plugin is particularly important for hyperlinks within the + formal document-model (\secref{sec:tooltips-hyperlinks}). Further plugins + (e.g.\ \<^emph>\ErrorList\, \<^emph>\Code2HTML\) are included to saturate the dependencies + of bundled plugins, but have no particular use in Isabelle/jEdit. \ subsection \Options \label{sec:options}\ @@ -497,13 +496,14 @@ paragraph \Encoding.\ text \Technically, the Unicode interpretation of Isabelle symbols is an \<^emph>\encoding\ called \<^verbatim>\UTF-8-Isabelle\ in jEdit (\<^emph>\not\ 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>\ISO-8859-15\. In that case, verbatim ``\<^verbatim>\\\'' will - be shown in the text buffer instead of its Unicode rendering ``\\\''. The - jEdit menu operation \<^emph>\File~/ Reload with Encoding~/ UTF-8-Isabelle\ helps - to resolve such problems (after repairing malformed parts of the text). \ + 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>\ISO-8859-15\. In that case, verbatim + ``\<^verbatim>\\\'' will be shown in the text buffer instead of its Unicode rendering + ``\\\''. The jEdit menu operation \<^emph>\File~/ Reload with Encoding~/ + UTF-8-Isabelle\ helps to resolve such problems (after repairing malformed + parts of the text). \ paragraph \Font.\ text \Correct rendering via Unicode requires a font that contains glyphs for diff -r aec5d9c88d69 -r 65ad7a7a9d6a src/Pure/Tools/main.scala --- a/src/Pure/Tools/main.scala Sun Aug 20 18:55:03 2017 +0200 +++ b/src/Pure/Tools/main.scala Sun Aug 20 23:41:17 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) { diff -r aec5d9c88d69 -r 65ad7a7a9d6a src/Pure/Tools/simplifier_trace.scala --- a/src/Pure/Tools/simplifier_trace.scala Sun Aug 20 18:55:03 2017 +0200 +++ b/src/Pure/Tools/simplifier_trace.scala Sun Aug 20 23:41:17 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 = diff -r aec5d9c88d69 -r 65ad7a7a9d6a src/Tools/jEdit/lib/Tools/jedit --- a/src/Tools/jEdit/lib/Tools/jedit Sun Aug 20 18:55:03 2017 +0200 +++ b/src/Tools/jEdit/lib/Tools/jedit Sun Aug 20 23:41:17 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 diff -r aec5d9c88d69 -r 65ad7a7a9d6a src/Tools/jEdit/src-base/isabelle_encoding.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src-base/isabelle_encoding.scala Sun Aug 20 23:41:17 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()) + } +} diff -r aec5d9c88d69 -r 65ad7a7a9d6a src/Tools/jEdit/src-base/plugin.scala --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src-base/plugin.scala Sun Aug 20 23:41:17 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() + } +} diff -r aec5d9c88d69 -r 65ad7a7a9d6a src/Tools/jEdit/src-base/services.xml --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Tools/jEdit/src-base/services.xml Sun Aug 20 23:41:17 2017 +0200 @@ -0,0 +1,8 @@ + + + + + + new isabelle.jedit_base.Isabelle_Encoding(); + + diff -r aec5d9c88d69 -r 65ad7a7a9d6a src/Tools/jEdit/src/Isabelle.props --- a/src/Tools/jEdit/src/Isabelle.props Sun Aug 20 18:55:03 2017 +0200 +++ b/src/Tools/jEdit/src/Isabelle.props Sun Aug 20 23:41:17 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 diff -r aec5d9c88d69 -r 65ad7a7a9d6a src/Tools/jEdit/src/isabelle_encoding.scala --- a/src/Tools/jEdit/src/isabelle_encoding.scala Sun Aug 20 18:55:03 2017 +0200 +++ b/src/Tools/jEdit/src/isabelle_encoding.scala Sun Aug 20 23:41:17 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()) - } -} diff -r aec5d9c88d69 -r 65ad7a7a9d6a src/Tools/jEdit/src/isabelle_options.scala --- a/src/Tools/jEdit/src/isabelle_options.scala Sun Aug 20 18:55:03 2017 +0200 +++ b/src/Tools/jEdit/src/isabelle_options.scala Sun Aug 20 23:41:17 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 = diff -r aec5d9c88d69 -r 65ad7a7a9d6a src/Tools/jEdit/src/jedit_editor.scala --- a/src/Tools/jEdit/src/jedit_editor.scala Sun Aug 20 18:55:03 2017 +0200 +++ b/src/Tools/jEdit/src/jedit_editor.scala Sun Aug 20 23:41:17 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() diff -r aec5d9c88d69 -r 65ad7a7a9d6a src/Tools/jEdit/src/jedit_sessions.scala --- a/src/Tools/jEdit/src/jedit_sessions.scala Sun Aug 20 18:55:03 2017 +0200 +++ b/src/Tools/jEdit/src/jedit_sessions.scala Sun Aug 20 23:41:17 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 diff -r aec5d9c88d69 -r 65ad7a7a9d6a src/Tools/jEdit/src/plugin.scala --- a/src/Tools/jEdit/src/plugin.scala Sun Aug 20 18:55:03 2017 +0200 +++ b/src/Tools/jEdit/src/plugin.scala Sun Aug 20 23:41:17 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() } } diff -r aec5d9c88d69 -r 65ad7a7a9d6a src/Tools/jEdit/src/services.xml --- a/src/Tools/jEdit/src/services.xml Sun Aug 20 18:55:03 2017 +0200 +++ b/src/Tools/jEdit/src/services.xml Sun Aug 20 23:41:17 2017 +0200 @@ -11,9 +11,6 @@ new isabelle.jedit.PIDE_Docking_Framework(); - - new isabelle.jedit.Isabelle_Encoding(); - new isabelle.jedit.Isabelle_Sidekick_Default(); diff -r aec5d9c88d69 -r 65ad7a7a9d6a src/Tools/jEdit/src/theories_dockable.scala --- a/src/Tools/jEdit/src/theories_dockable.scala Sun Aug 20 18:55:03 2017 +0200 +++ b/src/Tools/jEdit/src/theories_dockable.scala Sun Aug 20 23:41:17 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))