diff --git a/src/Pure/System/getopts.scala b/src/Pure/System/getopts.scala
--- a/src/Pure/System/getopts.scala
+++ b/src/Pure/System/getopts.scala
@@ -1,72 +1,72 @@
/* Title: Pure/System/getopts.scala
Author: Makarius
Support for command-line options as in GNU bash.
*/
package isabelle
import scala.annotation.tailrec
object Getopts
{
def apply(usage_text: String, option_specs: (String, String => Unit)*): Getopts =
{
val options =
option_specs.foldLeft(Map.empty[Char, (Boolean, String => Unit)]) {
case (m, (s, f)) =>
val (a, entry) =
- if (s.size == 1) (s(0), (false, f))
- else if (s.size == 2 && s.endsWith(":")) (s(0), (true, f))
+ if (s.length == 1) (s(0), (false, f))
+ else if (s.length == 2 && s.endsWith(":")) (s(0), (true, f))
else error("Bad option specification: " + quote(s))
if (m.isDefinedAt(a)) error("Duplicate option specification: " + quote(a.toString))
else m + (a -> entry)
}
new Getopts(usage_text, options)
}
}
class Getopts private(usage_text: String, options: Map[Char, (Boolean, String => Unit)])
{
def usage(): Nothing =
{
Output.writeln(usage_text, stdout = true)
sys.exit(1)
}
private def is_option(opt: Char): Boolean = options.isDefinedAt(opt)
private def is_option0(opt: Char): Boolean = is_option(opt) && !options(opt)._1
private def is_option1(opt: Char): Boolean = is_option(opt) && options(opt)._1
private def print_option(opt: Char): String = quote("-" + opt.toString)
private def option(opt: Char, opt_arg: List[Char]): Unit =
try { options(opt)._2.apply(opt_arg.mkString) }
catch {
case ERROR(msg) =>
cat_error(msg, "The error(s) above occurred in command-line option " + print_option(opt))
}
@tailrec private def getopts(args: List[List[Char]]): List[List[Char]] =
args match {
case List('-', '-') :: rest_args => rest_args
case ('-' :: opt :: rest_opts) :: rest_args if is_option0(opt) && rest_opts.nonEmpty =>
option(opt, Nil); getopts(('-' :: rest_opts) :: rest_args)
case List('-', opt) :: rest_args if is_option0(opt) =>
option(opt, Nil); getopts(rest_args)
case ('-' :: opt :: opt_arg) :: rest_args if is_option1(opt) && opt_arg.nonEmpty =>
option(opt, opt_arg); getopts(rest_args)
case List('-', opt) :: opt_arg :: rest_args if is_option1(opt) =>
option(opt, opt_arg); getopts(rest_args)
case List(List('-', opt)) if is_option1(opt) =>
Output.error_message("Command-line option " + print_option(opt) + " requires an argument")
usage()
case ('-' :: opt :: _) :: _ if !is_option(opt) =>
if (opt != '?') Output.error_message("Illegal command-line option " + print_option(opt))
usage()
case _ => args
}
def apply(args: List[String]): List[String] = getopts(args.map(_.toList)).map(_.mkString)
def apply(args: Array[String]): List[String] = apply(args.toList)
}
diff --git a/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala b/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala
--- a/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala
+++ b/src/Tools/jEdit/jedit_main/isabelle_sidekick.scala
@@ -1,305 +1,308 @@
/* Title: Tools/jEdit/src/isabelle_sidekick.scala
Author: Fabian Immler, TU Munich
Author: Makarius
SideKick parsers for Isabelle proof documents.
*/
package isabelle.jedit_main
import isabelle._
import isabelle.jedit._
import javax.swing.tree.DefaultMutableTreeNode
import javax.swing.text.Position
-import javax.swing.{JLabel, Icon}
+import javax.swing.Icon
import org.gjt.sp.jedit.Buffer
import sidekick.{SideKickParser, SideKickParsedData, IAsset}
object Isabelle_Sidekick
{
def int_to_pos(offset: Text.Offset): Position =
- new Position { def getOffset = offset; override def toString: String = offset.toString }
+ new Position {
+ def getOffset: Text.Offset = offset
+ override def toString: String = offset.toString
+ }
def root_data(buffer: Buffer): SideKickParsedData =
{
val data = new SideKickParsedData(buffer.getName)
data.getAsset(data.root).setEnd(int_to_pos(buffer.getLength))
data
}
class Keyword_Asset(keyword: String, text: String, range: Text.Range) extends IAsset
{
private val css = GUI.imitate_font_css(GUI.label_font())
- protected var _name = text
- protected var _start = int_to_pos(range.start)
- protected var _end = int_to_pos(range.stop)
+ protected var _name: String = text
+ protected var _start: Position = int_to_pos(range.start)
+ protected var _end: Position = int_to_pos(range.stop)
override def getIcon: Icon = null
override def getShortString: String =
{
val n = keyword.length
val s =
_name.indexOf(keyword) match {
case i if i >= 0 && n > 0 =>
HTML.output(_name.substring(0, i)) +
"" + HTML.output(keyword) + "" +
HTML.output(_name.substring(i + n))
case _ => HTML.output(_name)
}
"" + s + ""
}
override def getLongString: String = _name
override def getName: String = _name
override def setName(name: String): Unit = _name = name
override def getStart: Position = _start
override def setStart(start: Position): Unit = _start = start
override def getEnd: Position = _end
override def setEnd(end: Position): Unit = _end = end
override def toString: String = _name
}
class Asset(name: String, range: Text.Range) extends Keyword_Asset("", name, range)
def swing_markup_tree(tree: Markup_Tree, parent: DefaultMutableTreeNode,
swing_node: Text.Info[List[XML.Elem]] => DefaultMutableTreeNode): Unit =
{
for ((_, entry) <- tree.branches) {
val node = swing_node(Text.Info(entry.range, entry.markup))
swing_markup_tree(entry.subtree, node, swing_node)
parent.add(node)
}
}
}
class Isabelle_Sidekick(name: String) extends SideKickParser(name)
{
override def supportsCompletion = false
/* parsing */
@volatile protected var stopped = false
- override def stop() = { stopped = true }
+ override def stop(): Unit = { stopped = true }
def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean = false
def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
{
stopped = false
// FIXME lock buffer (!??)
val data = Isabelle_Sidekick.root_data(buffer)
val syntax = Isabelle.buffer_syntax(buffer)
val ok =
if (syntax.isDefined) {
val ok = parser(buffer, syntax.get, data)
if (stopped) { data.root.add(new DefaultMutableTreeNode("")); true }
else ok
}
else false
if (!ok) data.root.add(new DefaultMutableTreeNode(""))
data
}
}
class Isabelle_Sidekick_Structure(
name: String,
node_name: Buffer => Option[Document.Node.Name],
parse: (Outer_Syntax, Document.Node.Name, CharSequence) => List[Document_Structure.Document])
extends Isabelle_Sidekick(name)
{
override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
{
def make_tree(
parent: DefaultMutableTreeNode,
offset: Text.Offset,
documents: List[Document_Structure.Document]): Unit =
{
documents.foldLeft(offset) {
case (i, document) =>
document match {
case Document_Structure.Block(name, text, body) =>
val range = Text.Range(i, i + document.length)
val node =
new DefaultMutableTreeNode(
new Isabelle_Sidekick.Keyword_Asset(name, Library.first_line(text), range))
parent.add(node)
make_tree(node, i, body)
case _ =>
}
i + document.length
}
}
node_name(buffer) match {
case Some(name) =>
make_tree(data.root, 0, parse(syntax, name, JEdit_Lib.buffer_text(buffer)))
true
case None =>
false
}
}
}
class Isabelle_Sidekick_Default extends
Isabelle_Sidekick_Structure("isabelle",
PIDE.resources.theory_node_name, Document_Structure.parse_sections)
class Isabelle_Sidekick_Context extends
Isabelle_Sidekick_Structure("isabelle-context",
PIDE.resources.theory_node_name, Document_Structure.parse_blocks)
class Isabelle_Sidekick_Options extends
Isabelle_Sidekick_Structure("isabelle-options",
_ => Some(Document.Node.Name("options")), Document_Structure.parse_sections)
class Isabelle_Sidekick_Root extends
Isabelle_Sidekick_Structure("isabelle-root",
_ => Some(Document.Node.Name("ROOT")), Document_Structure.parse_sections)
class Isabelle_Sidekick_ML extends
Isabelle_Sidekick_Structure("isabelle-ml",
buffer => Some(PIDE.resources.node_name(buffer)),
(_, _, text) => Document_Structure.parse_ml_sections(false, text))
class Isabelle_Sidekick_SML extends
Isabelle_Sidekick_Structure("isabelle-sml",
buffer => Some(PIDE.resources.node_name(buffer)),
(_, _, text) => Document_Structure.parse_ml_sections(true, text))
class Isabelle_Sidekick_Markup extends Isabelle_Sidekick("isabelle-markup")
{
override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
{
val opt_snapshot =
Document_Model.get(buffer) match {
case Some(model) if model.is_theory => Some(model.snapshot())
case _ => None
}
opt_snapshot match {
case Some(snapshot) =>
for ((command, command_start) <- snapshot.node.command_iterator() if !stopped) {
val markup =
snapshot.state.command_markup(
snapshot.version, command, Command.Markup_Index.markup,
command.range, Markup.Elements.full)
Isabelle_Sidekick.swing_markup_tree(markup, data.root,
(info: Text.Info[List[XML.Elem]]) =>
{
val range = info.range + command_start
val content = command.source(info.range).replace('\n', ' ')
val info_text = Pretty.formatted(Pretty.fbreaks(info.info), margin = 40.0).mkString
new DefaultMutableTreeNode(
new Isabelle_Sidekick.Asset(command.toString, range) {
override def getShortString: String = content
override def getLongString: String = info_text
override def toString: String = quote(content) + " " + range.toString
})
})
}
true
case None => false
}
}
}
class Isabelle_Sidekick_News extends Isabelle_Sidekick("isabelle-news")
{
private val Heading1 = """^New in (.*)\w*$""".r
private val Heading2 = """^\*\*\*\w*(.*)\w*\*\*\*\w*$""".r
private def make_node(s: String, start: Text.Offset, stop: Text.Offset): DefaultMutableTreeNode =
new DefaultMutableTreeNode(new Isabelle_Sidekick.Asset(s, Text.Range(start, stop)))
override def parser(buffer: Buffer, syntax: Outer_Syntax, data: SideKickParsedData): Boolean =
{
var offset = 0
var end_offset = 0
var start1: Option[(Int, String, Vector[DefaultMutableTreeNode])] = None
var start2: Option[(Int, String)] = None
- def close1: Unit =
+ def close1(): Unit =
start1 match {
case Some((start_offset, s, body)) =>
val node = make_node(s, start_offset, end_offset)
body.foreach(node.add(_))
data.root.add(node)
start1 = None
case None =>
}
- def close2: Unit =
+ def close2(): Unit =
start2 match {
case Some((start_offset, s)) =>
start1 match {
case Some((start_offset1, s1, body)) =>
val node = make_node(s, start_offset, end_offset)
start1 = Some((start_offset1, s1, body :+ node))
case None =>
}
start2 = None
case None =>
}
for (line <- split_lines(JEdit_Lib.buffer_text(buffer)) if !stopped) {
line match {
- case Heading1(s) => close2; close1; start1 = Some((offset, s, Vector()))
- case Heading2(s) => close2; start2 = Some((offset, s))
+ case Heading1(s) => close2(); close1(); start1 = Some((offset, s, Vector()))
+ case Heading2(s) => close2(); start2 = Some((offset, s))
case _ =>
}
offset += line.length + 1
if (!line.forall(Character.isSpaceChar)) end_offset = offset
}
- if (!stopped) { close2; close1 }
+ if (!stopped) { close2(); close1() }
true
}
}
class Isabelle_Sidekick_Bibtex extends SideKickParser("bibtex")
{
override def supportsCompletion = false
private class Asset(label: String, label_html: String, range: Text.Range, source: String)
extends Isabelle_Sidekick.Asset(label, range) {
override def getShortString: String = label_html
override def getLongString: String = source
}
def parse(buffer: Buffer, error_source: errorlist.DefaultErrorSource): SideKickParsedData =
{
val data = Isabelle_Sidekick.root_data(buffer)
try {
var offset = 0
for (chunk <- Bibtex.parse(JEdit_Lib.buffer_text(buffer))) {
val kind = chunk.kind
val name = chunk.name
val source = chunk.source
if (kind != "") {
val label = kind + (if (name == "") "" else " " + name)
val label_html =
"" + HTML.output(kind) + "" +
(if (name == "") "" else " " + HTML.output(name)) + ""
val range = Text.Range(offset, offset + source.length)
val asset = new Asset(label, label_html, range, source)
data.root.add(new DefaultMutableTreeNode(asset))
}
offset += source.length
}
data
}
catch { case ERROR(msg) => Output.warning(msg); null }
}
}
diff --git a/src/Tools/jEdit/jedit_main/scala_console.scala b/src/Tools/jEdit/jedit_main/scala_console.scala
--- a/src/Tools/jEdit/jedit_main/scala_console.scala
+++ b/src/Tools/jEdit/jedit_main/scala_console.scala
@@ -1,182 +1,182 @@
/* Title: Tools/jEdit/jedit_main/scala_console.scala
Author: Makarius
Scala instance of Console plugin.
*/
package isabelle.jedit_main
import isabelle._
import isabelle.jedit._
import console.{Console, ConsolePane, Shell, Output}
import org.gjt.sp.jedit.JARClassLoader
import java.io.{OutputStream, Writer, PrintWriter}
class Scala_Console extends Shell("Scala")
{
/* global state -- owned by GUI thread */
@volatile private var interpreters = Map.empty[Console, Interpreter]
@volatile private var global_console: Console = null
@volatile private var global_out: Output = null
@volatile private var global_err: Output = null
private val console_stream = new OutputStream
{
val buf = new StringBuilder(100)
override def flush(): Unit =
{
val s = buf.synchronized { val s = buf.toString; buf.clear(); s }
val str = UTF8.decode_permissive(s)
GUI_Thread.later {
if (global_out == null) java.lang.System.out.print(str)
else global_out.writeAttrs(null, str)
}
Time.seconds(0.01).sleep() // FIXME adhoc delay to avoid loosing output
}
override def close(): Unit = flush()
def write(byte: Int): Unit =
{
val c = byte.toChar
buf.synchronized { buf.append(c) }
if (c == '\n') flush()
}
}
private val console_writer = new Writer
{
def flush(): Unit = console_stream.flush()
def close(): Unit = console_stream.flush()
def write(cbuf: Array[Char], off: Int, len: Int): Unit =
{
if (len > 0) {
UTF8.bytes(new String(cbuf.slice(off, off + len))).foreach(console_stream.write(_))
}
}
}
private def with_console[A](console: Console, out: Output, err: Output)(e: => A): A =
{
global_console = console
global_out = out
global_err = if (err == null) out else err
try {
scala.Console.withErr(console_stream) {
scala.Console.withOut(console_stream) { e }
}
}
finally {
- console_stream.flush
+ console_stream.flush()
global_console = null
global_out = null
global_err = null
}
}
private def report_error(str: String): Unit =
{
if (global_console == null || global_err == null) isabelle.Output.writeln(str)
else GUI_Thread.later { global_err.print(global_console.getErrorColor, str) }
}
/* interpreter thread */
private abstract class Request
private case class Start(console: Console) extends Request
private case class Execute(console: Console, out: Output, err: Output, command: String)
extends Request
private class Interpreter
{
private val running = Synchronized[Option[Thread]](None)
def interrupt(): Unit = running.change(opt => { opt.foreach(_.interrupt()); opt })
private val interp =
Scala.Compiler.context(error = report_error, jar_dirs = JEdit_Lib.directories).
interpreter(
print_writer = new PrintWriter(console_writer, true),
class_loader = new JARClassLoader)
val thread: Consumer_Thread[Request] = Consumer_Thread.fork("Scala_Console")
{
case Start(console) =>
interp.bind("view", "org.gjt.sp.jedit.View", console.getView)
interp.bind("console", "console.Console", console)
interp.interpret("import isabelle._; import isabelle.jedit._")
true
case Execute(console, out, err, command) =>
with_console(console, out, err) {
try {
running.change(_ => Some(Thread.currentThread()))
interp.interpret(command)
}
finally {
running.change(_ => None)
Exn.Interrupt.dispose()
}
GUI_Thread.later {
if (err != null) err.commandDone()
out.commandDone()
}
true
}
}
}
/* jEdit console methods */
override def openConsole(console: Console): Unit =
{
val interp = new Interpreter
interp.thread.send(Start(console))
interpreters += (console -> interp)
}
override def closeConsole(console: Console): Unit =
{
interpreters.get(console) match {
case Some(interp) =>
interp.interrupt()
interp.thread.shutdown()
interpreters -= console
case None =>
}
}
override def printInfoMessage(out: Output): Unit =
{
out.print(null,
"This shell evaluates Isabelle/Scala expressions.\n\n" +
"The contents of package isabelle and isabelle.jedit are imported.\n" +
"The following special toplevel bindings are provided:\n" +
" view -- current jEdit/Swing view (e.g. view.getBuffer, view.getTextArea)\n" +
" console -- jEdit Console plugin\n" +
" PIDE -- Isabelle/PIDE plugin (e.g. PIDE.session, PIDE.snapshot, PIDE.rendering)\n")
}
override def printPrompt(console: Console, out: Output): Unit =
{
out.writeAttrs(ConsolePane.colorAttributes(console.getInfoColor), "scala>")
out.writeAttrs(ConsolePane.colorAttributes(console.getPlainColor), " ")
}
override def execute(
console: Console, input: String, out: Output, err: Output, command: String): Unit =
{
interpreters(console).thread.send(Execute(console, out, err, command))
}
override def stop(console: Console): Unit =
interpreters.get(console).foreach(_.interrupt())
}
diff --git a/src/Tools/jEdit/src/main.scala b/src/Tools/jEdit/src/main.scala
--- a/src/Tools/jEdit/src/main.scala
+++ b/src/Tools/jEdit/src/main.scala
@@ -1,142 +1,142 @@
/* Title: src/Tools/jEdit/src/main.scala
Author: Makarius
Main Isabelle application entry point.
*/
package isabelle.jedit
import isabelle._
import org.gjt.sp.jedit.{MiscUtilities, jEdit}
object Main
{
/* main entry point */
def main(args: Array[String]): Unit =
{
if (args.nonEmpty && args(0) == "-init") {
Isabelle_System.init()
}
else {
val start =
{
try {
Isabelle_System.init()
Isabelle_Fonts.init()
GUI.init_lafs()
/* ROOTS template */
{
val roots = Path.explode("$ISABELLE_HOME_USER/ROOTS")
if (!roots.is_file) File.write(roots, """# Additional session root directories
#
# * each line contains one directory entry in Isabelle path notation, e.g.
#
# $ISABELLE_HOME/../AFP/thys
#
# for a copy of AFP put side-by-side to the Isabelle distribution
#
# * Isabelle/jEdit provides formal markup for C-hover-click and completion
#
# * lines starting with "#" are stripped
#
# * changes require restart of the Isabelle application
#
#:mode=text:encoding=UTF-8:
#$ISABELLE_HOME/../AFP/thys
""")
}
/* 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.make_directory(settings_dir + Path.explode("DockableWindowManager"))
if (!(settings_dir + Path.explode("perspective.xml")).is_file) {
File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"),
"""""")
File.write(settings_dir + Path.explode("perspective.xml"),
XML.header +
"""
""")
}
Scala_Project.plugin_contexts().foreach(isabelle.setup.Build.build(_, false))
/* args */
val jedit_settings =
"-settings=" + File.platform_path(Path.explode("$JEDIT_SETTINGS"))
val jedit_server =
System.getProperty("isabelle.jedit_server") match {
case null | "" => "-noserver"
case name => "-server=" + name
}
val jedit_options =
Isabelle_System.getenv_strict("JEDIT_OPTIONS").split(" +")
val more_args =
{
args.toList.dropWhile(arg => arg.startsWith("-") && arg != "--") match {
case Nil | List("--") =>
args ++ Array(File.platform_path(Path.explode("$USER_HOME/Scratch.thy")))
- case List(":") => args.slice(0, args.size - 1)
+ case List(":") => args.slice(0, args.length - 1)
case _ => args
}
}
/* environment */
for (name <- List("ISABELLE_HOME", "ISABELLE_HOME_USER", "JEDIT_HOME", "JEDIT_SETTINGS")) {
MiscUtilities.putenv(name, File.platform_path(Isabelle_System.getenv(name)))
}
MiscUtilities.putenv("ISABELLE_ROOT", null)
/* properties */
System.setProperty("jedit.home", File.platform_path(Path.explode("$JEDIT_HOME")))
System.setProperty("scala.home", File.platform_path(Path.explode("$SCALA_HOME")))
System.setProperty("scala.color", "false")
/* main startup */
() => jEdit.main(Array(jedit_settings, jedit_server) ++ jedit_options ++ more_args)
}
catch {
case exn: Throwable =>
GUI.init_laf()
GUI.dialog(null, "Isabelle", GUI.scrollable_text(Exn.message(exn)))
sys.exit(2)
}
}
start()
}
}
}
diff --git a/src/Tools/jEdit/src/main_plugin.scala b/src/Tools/jEdit/src/main_plugin.scala
--- a/src/Tools/jEdit/src/main_plugin.scala
+++ b/src/Tools/jEdit/src/main_plugin.scala
@@ -1,501 +1,501 @@
/* Title: Tools/jEdit/src/main_plugin.scala
Author: Makarius
Main plumbing for PIDE infrastructure as jEdit plugin.
*/
package isabelle.jedit
import isabelle._
import javax.swing.JOptionPane
import java.io.{File => JFile}
import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, PerspectiveManager}
import org.gjt.sp.jedit.textarea.JEditTextArea
import org.gjt.sp.jedit.syntax.ModeProvider
import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged,
ViewUpdate}
import org.gjt.sp.util.SyntaxUtilities
import org.gjt.sp.util.Log
object PIDE
{
/* semantic document content */
def maybe_snapshot(view: View = null): Option[Document.Snapshot] = GUI_Thread.now
{
val buffer = JEdit_Lib.jedit_view(view).getBuffer
Document_Model.get(buffer).map(_.snapshot())
}
def maybe_rendering(view: View = null): Option[JEdit_Rendering] = GUI_Thread.now
{
val text_area = JEdit_Lib.jedit_view(view).getTextArea
Document_View.get(text_area).map(_.get_rendering())
}
def snapshot(view: View = null): Document.Snapshot =
maybe_snapshot(view) getOrElse error("No document model for current buffer")
def rendering(view: View = null): JEdit_Rendering =
maybe_rendering(view) getOrElse error("No document view for current text area")
/* plugin instance */
@volatile var _plugin: Main_Plugin = null
def plugin: Main_Plugin =
if (_plugin == null) error("Uninitialized Isabelle/jEdit plugin")
else _plugin
def options: JEdit_Options = plugin.options
def resources: JEdit_Resources = plugin.resources
def session: Session = plugin.session
object editor extends JEdit_Editor
}
class Main_Plugin extends EBPlugin
{
/* options */
private var _options: JEdit_Options = null
private def init_options(): Unit =
_options = new JEdit_Options(Options.init())
def options: JEdit_Options = _options
/* resources */
private var _resources: JEdit_Resources = null
private def init_resources(): Unit = _resources = JEdit_Resources(options.value)
def resources: JEdit_Resources = _resources
/* session */
private var _session: Session = null
private def init_session(): Unit = _session = new Session(options.value, resources)
def session: Session = _session
/* misc support */
val completion_history = new Completion.History_Variable
val spell_checker = new Spell_Checker_Variable
/* global changes */
def options_changed(): Unit =
{
session.global_options.post(Session.Global_Options(options.value))
delay_load.invoke()
}
def deps_changed(): Unit =
{
delay_load.invoke()
}
/* theory files */
- lazy val delay_init =
+ lazy val delay_init: Delay =
Delay.last(options.seconds("editor_load_delay"), gui = true)
{
init_models()
}
private val delay_load_active = Synchronized(false)
private def delay_load_activated(): Boolean =
delay_load_active.guarded_access(a => Some((!a, true)))
private def delay_load_action(): Unit =
{
if (Isabelle.continuous_checking && delay_load_activated() &&
PerspectiveManager.isPerspectiveEnabled)
{
if (JEdit_Lib.jedit_buffers().exists(_.isLoading)) delay_load.invoke()
else {
val required_files =
{
val models = Document_Model.get_models()
val thys =
(for ((node_name, model) <- models.iterator if model.is_theory)
yield (node_name, Position.none)).toList
val thy_files1 = resources.dependencies(thys).theories
val thy_files2 =
(for {
(name, _) <- models.iterator
thy_name <- resources.make_theory_name(name)
} yield thy_name).toList
val aux_files =
if (options.bool("jedit_auto_resolve")) {
val stable_tip_version =
if (models.forall(p => p._2.is_stable))
session.get_state().stable_tip_version
else None
stable_tip_version match {
case Some(version) => resources.undefined_blobs(version.nodes)
case None => delay_load.invoke(); Nil
}
}
else Nil
(thy_files1 ::: thy_files2 ::: aux_files).filterNot(models.isDefinedAt)
}
if (required_files.nonEmpty) {
try {
Isabelle_Thread.fork(name = "resolve_dependencies") {
val loaded_files =
for {
name <- required_files
text <- resources.read_file_content(name)
} yield (name, text)
GUI_Thread.later {
try {
Document_Model.provide_files(session, loaded_files)
delay_init.invoke()
}
finally { delay_load_active.change(_ => false) }
}
}
}
catch { case _: Throwable => delay_load_active.change(_ => false) }
}
else delay_load_active.change(_ => false)
}
}
}
private lazy val delay_load =
Delay.last(options.seconds("editor_load_delay"), gui = true) { delay_load_action() }
private def file_watcher_action(changed: Set[JFile]): Unit =
if (Document_Model.sync_files(changed)) PIDE.editor.invoke_generated()
lazy val file_watcher: File_Watcher =
File_Watcher(file_watcher_action, options.seconds("editor_load_delay"))
/* session phase */
val session_phase_changed: Session.Consumer[Session.Phase] = Session.Consumer("Isabelle/jEdit")
{
case Session.Terminated(result) if !result.ok =>
GUI_Thread.later {
GUI.error_dialog(jEdit.getActiveView, "Prover process terminated with error",
"Isabelle Syslog", GUI.scrollable_text(session.syslog_content()))
}
case Session.Ready if !shutting_down.value =>
init_models()
if (!Isabelle.continuous_checking) {
GUI_Thread.later {
val answer =
GUI.confirm_dialog(jEdit.getActiveView,
"Continuous checking of PIDE document",
JOptionPane.YES_NO_OPTION,
"Continuous checking is presently disabled:",
"editor buffers will remain inactive!",
"Enable continuous checking now?")
if (answer == 0) Isabelle.continuous_checking = true
}
}
delay_load.invoke()
case Session.Shutdown =>
GUI_Thread.later {
delay_load.revoke()
delay_init.revoke()
PIDE.editor.shutdown()
exit_models(JEdit_Lib.jedit_buffers().toList)
}
case _ =>
}
/* document model and view */
def exit_models(buffers: List[Buffer]): Unit =
{
GUI_Thread.now {
buffers.foreach(buffer =>
JEdit_Lib.buffer_lock(buffer) {
JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit)
Document_Model.exit(buffer)
})
}
}
def init_models(): Unit =
{
GUI_Thread.now {
PIDE.editor.flush()
for {
buffer <- JEdit_Lib.jedit_buffers()
if buffer != null && !buffer.getBooleanProperty(Buffer.GZIPPED)
} {
if (buffer.isLoaded) {
JEdit_Lib.buffer_lock(buffer) {
val node_name = resources.node_name(buffer)
val model = Document_Model.init(session, node_name, buffer)
for {
text_area <- JEdit_Lib.jedit_text_areas(buffer)
if Document_View.get(text_area).map(_.model) != Some(model)
} Document_View.init(model, text_area)
}
}
else delay_init.invoke()
}
PIDE.editor.invoke_generated()
}
}
def init_view(buffer: Buffer, text_area: JEditTextArea): Unit =
GUI_Thread.now {
JEdit_Lib.buffer_lock(buffer) {
Document_Model.get(buffer) match {
case Some(model) => Document_View.init(model, text_area)
case None =>
}
}
}
def exit_view(buffer: Buffer, text_area: JEditTextArea): Unit =
GUI_Thread.now {
JEdit_Lib.buffer_lock(buffer) {
Document_View.exit(text_area)
}
}
/* main plugin plumbing */
@volatile private var startup_failure: Option[Throwable] = None
@volatile private var startup_notified = false
private def init_editor(view: View): Unit =
{
Keymap_Merge.check_dialog(view)
Session_Build.check_dialog(view)
}
private def init_title(view: View): Unit =
{
val title =
proper_string(Isabelle_System.getenv("ISABELLE_IDENTIFIER")).getOrElse("Isabelle") +
"/" + PIDE.resources.session_name
val marker = "\u200B"
val old_title = view.getViewConfig.title
if (old_title == null || old_title.startsWith(marker)) {
view.setUserTitle(marker + title)
}
}
override def handleMessage(message: EBMessage): Unit =
{
GUI_Thread.assert {}
if (startup_failure.isDefined && !startup_notified) {
message match {
case msg: EditorStarted =>
GUI.error_dialog(null, "Isabelle plugin startup failure",
GUI.scrollable_text(Exn.message(startup_failure.get)),
"Prover IDE inactive!")
startup_notified = true
case _ =>
}
}
if (startup_failure.isEmpty) {
message match {
case msg: EditorStarted =>
if (resources.session_errors.nonEmpty) {
GUI.warning_dialog(jEdit.getActiveView,
"Bad session structure: may cause problems with theory imports",
GUI.scrollable_text(cat_lines(resources.session_errors)))
}
jEdit.propertiesChanged()
val view = jEdit.getActiveView()
init_editor(view)
PIDE.editor.hyperlink_position(true, Document.Snapshot.init,
JEdit_Sessions.logic_root(options.value)).foreach(_.follow(view))
case msg: ViewUpdate
if msg.getWhat == ViewUpdate.CREATED && msg.getView != null =>
init_title(msg.getView)
case msg: BufferUpdate
if msg.getWhat == BufferUpdate.LOAD_STARTED || msg.getWhat == BufferUpdate.CLOSING =>
if (msg.getBuffer != null) {
exit_models(List(msg.getBuffer))
PIDE.editor.invoke_generated()
}
case msg: BufferUpdate
if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED || msg.getWhat == BufferUpdate.LOADED =>
if (session.is_ready) {
delay_init.invoke()
delay_load.invoke()
}
case msg: EditPaneUpdate
if msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
msg.getWhat == EditPaneUpdate.CREATED ||
msg.getWhat == EditPaneUpdate.DESTROYED =>
val edit_pane = msg.getEditPane
val buffer = edit_pane.getBuffer
val text_area = edit_pane.getTextArea
if (buffer != null && text_area != null) {
if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
msg.getWhat == EditPaneUpdate.CREATED) {
if (session.is_ready)
init_view(buffer, text_area)
}
else {
Isabelle.dismissed_popups(text_area.getView)
exit_view(buffer, text_area)
}
if (msg.getWhat == EditPaneUpdate.CREATED)
Completion_Popup.Text_Area.init(text_area)
if (msg.getWhat == EditPaneUpdate.DESTROYED)
Completion_Popup.Text_Area.exit(text_area)
}
case msg: PropertiesChanged =>
for {
view <- JEdit_Lib.jedit_views()
edit_pane <- JEdit_Lib.jedit_edit_panes(view)
} {
val buffer = edit_pane.getBuffer
val text_area = edit_pane.getTextArea
if (buffer != null && text_area != null) init_view(buffer, text_area)
}
spell_checker.update(options.value)
session.update_options(options.value)
case _ =>
}
}
}
/* mode provider */
private var orig_mode_provider: ModeProvider = null
private var pide_mode_provider: ModeProvider = null
def init_mode_provider(): Unit =
{
orig_mode_provider = ModeProvider.instance
if (orig_mode_provider.isInstanceOf[ModeProvider]) {
pide_mode_provider = new Token_Markup.Mode_Provider(orig_mode_provider)
ModeProvider.instance = pide_mode_provider
}
}
def exit_mode_provider(): Unit =
{
if (ModeProvider.instance == pide_mode_provider)
ModeProvider.instance = orig_mode_provider
}
/* HTTP server */
val http_root: String = "/" + UUID.random()
val http_server: HTTP.Server = HTTP.server(Document_Model.http_handlers(http_root))
/* start and stop */
private val shutting_down = Synchronized(false)
override def start(): Unit =
{
/* strict initialization */
init_options()
init_resources()
init_session()
PIDE._plugin = this
/* non-strict initialization */
try {
completion_history.load()
spell_checker.update(options.value)
JEdit_Lib.jedit_views().foreach(init_title)
Syntax_Style.set_extender(Syntax_Style.Main_Extender)
init_mode_provider()
JEdit_Lib.jedit_text_areas().foreach(Completion_Popup.Text_Area.init)
http_server.start()
startup_failure = None
}
catch {
case exn: Throwable =>
startup_failure = Some(exn)
startup_notified = false
Log.log(Log.ERROR, this, exn)
}
shutting_down.change(_ => false)
val view = jEdit.getActiveView()
if (view != null) init_editor(view)
}
override def stop(): Unit =
{
http_server.stop()
Syntax_Style.set_extender(Syntax_Style.Base_Extender)
exit_mode_provider()
JEdit_Lib.jedit_text_areas().foreach(Completion_Popup.Text_Area.exit)
if (startup_failure.isEmpty) {
options.value.save_prefs()
completion_history.value.save()
}
exit_models(JEdit_Lib.jedit_buffers().toList)
shutting_down.change(_ => true)
session.stop()
file_watcher.shutdown()
PIDE.editor.shutdown()
Document_Model.reset()
}
}