# HG changeset patch # User wenzelm # Date 1258218840 -3600 # Node ID 8d43e5e0588d5e52e3ab8936cbfef55bdaa75525 # Parent 0c5d1485dea796f091c40fae287f20e5d4ce5f61 dismantled remains of old jEdit plugin; diff -r 0c5d1485dea7 -r 8d43e5e0588d lib/jedit/README --- a/lib/jedit/README Sat Nov 14 17:49:29 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,50 +0,0 @@ -Isabelle support for jEdit -- http://www.jedit.org/ -=================================================== - -This provides both a basic editing "mode" (with some degree of syntax -highlighting), and a minimal "plugin" with some support for -interaction with the Isabelle process. - - -Mode installation ------------------ - -1) Copy or symlink [ISABELLE_HOME]/lib/jedit/isabelle.xml to -[JEDIT_SETTINGS]/modes/ - -2) Add the following entry [JEDIT_SETTINGS]/modes/catalog - - - -Example catalog file: - - - - - - - - -Plugin installation -------------------- - -1) Install copies of the Isabelle jars: - - [ISABELLE_HOME]/lib/classes/Pure.jar -> [JEDIT_SETTINGS]/jars/isabelle-Pure.jar - [ISABELLE_HOME]/lib/jedit/isabelle.jar -> [JEDIT_SETTINGS]/jars/isabelle.jar - -2) Install scala-library.jar from the regular Scala distribution, -cf. the http://www.scala-lang.org/downloads/index.html as - - [JEDIT_SETTINGS]/jars/isabelle-scala-library.jar - -3) Enable the plugin using the manager of jEdit; invoke the "isabelle" -editor action. The resulting window may be docked, e.g. at bottom. - -Note that the Errorlist plugin provides some useful options like "Show -error icons in the gutter", for immediate feedback of Isabelle -warnings and errors in the source text. The Errorlist window may be -docked likewise. - - -$Id$ diff -r 0c5d1485dea7 -r 8d43e5e0588d lib/jedit/isabelle.xml --- a/lib/jedit/isabelle.xml Sat Nov 14 17:49:29 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,347 +0,0 @@ - - - - - - - - - - - - - - - - - - - (* - *) - - - {* - *} - - - ` - ` - - - " - " - - - . - .. - Isabelle.command - Isar.begin_document - Isar.define_command - Isar.edit_document - Isar.end_document - ML - ML_command - ML_prf - ML_val - abbreviation - actions - advanced - also - and - apply - apply_end - arities - assume - assumes - atom_decl - atp_info - atp_kill - atp_messages - atp_minimize - attach - attribute_setup - automaton - avoids - ax_specification - axclass - axiomatization - axioms - back - begin - binder - by - cannot_undo - case - case_eqns - cd - chapter - class - class_deps - classes - classrel - codatatype - code_abort - code_class - code_const - code_datatype - code_deps - code_include - code_instance - code_library - code_module - code_modulename - code_monad - code_pred - code_reserved - code_thms - code_type - coinductive - coinductive_set - commit - compose - con_defs - congs - constdefs - constrains - consts - consts_code - contains - context - corollary - cpodef - datatype - declaration - declare - def - defaultsort - defer - defer_recdef - defines - definition - defs - disable_pr - display_drafts - domain - domains - done - elimination - enable_pr - end - equivariance - exit - export_code - extract - extract_type - file - finalconsts - finally - find_consts - find_theorems - fix - fixes - fixpat - fixrec - for - from - full_prf - fun - function - global - guess - have - header - help - hence - hide - hide_action - hints - identifier - if - imports - in - induction - inductive - inductive_cases - inductive_set - infix - infixl - infixr - init_toplevel - initially - inputs - instance - instantiation - internals - interpret - interpretation - intros - is - judgment - kill - kill_thy - lazy - lemma - lemmas - let - linear_undo - local - local_setup - locale - method_setup - module_name - monos - moreover - morphisms - next - nitpick - nitpick_params - no_notation - no_syntax - no_translations - nominal_datatype - nominal_inductive - nominal_inductive2 - nominal_primrec - nonterminals - normal_form - notation - note - notes - obtain - obtains - oops - open - oracle - output - outputs - overloaded - overloading - parse_ast_translation - parse_translation - pcpodef - permissive - post - pr - pre - prefer - presume - pretty_setmargin - prf - primrec - print_abbrevs - print_antiquotations - print_ast_translation - print_atps - print_attributes - print_binds - print_cases - print_claset - print_classes - print_codeproc - print_codesetup - print_commands - print_configs - print_context - print_drafts - print_facts - print_induct_rules - print_interps - print_locale - print_locales - print_methods - print_orders - print_rules - print_simpset - print_statement - print_syntax - print_tcset - print_theorems - print_theory - print_trans_rules - print_translation - proof - prop - pwd - qed - quickcheck - quickcheck_params - quit - realizability - realizers - recdef - recdef_tc - record - recursor_eqns - refute - refute_params - remove_thy - rename - rep_datatype - restrict - sect - section - setup - show - shows - signature - simproc_setup - sledgehammer - sorry - specification - states - statespace - structure - subclass - sublocale - subsect - subsection - subsubsect - subsubsection - syntax - term - termination - text - text_raw - then - theorem - theorems - theory - thm - thm_deps - thus - thy_deps - to - touch_thy - transitions - translations - transrel - txt - txt_raw - typ - type_elims - type_intros - typed_print_translation - typedecl - typedef - types - types_code - ultimately - unchecked - undo - undos_proof - unfolding - unused_thms - use - use_thy - uses - using - value - values - welcome - where - with - { - } - - - diff -r 0c5d1485dea7 -r 8d43e5e0588d lib/jedit/plugin/Isabelle.props --- a/lib/jedit/plugin/Isabelle.props Sat Nov 14 17:49:29 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,32 +0,0 @@ -## Isabelle plugin properties -## $Id$ - -#identification -plugin.isabelle.jedit.IsabellePlugin.name = Isabelle -plugin.isabelle.jedit.IsabellePlugin.author = Makarius -plugin.isabelle.jedit.IsabellePlugin.version = 0.0.1 -plugin.isabelle.jedit.IsabellePlugin.description = Basic Isabelle support - -#system parameters -plugin.isabelle.jedit.IsabellePlugin.activate = defer -plugin.isabelle.jedit.IsabellePlugin.usePluginHome = false -plugin.isabelle.jedit.IsabellePlugin.jars = isabelle-Pure.jar isabelle-scala-library.jar - -#dependencies -plugin.isabelle.jedit.IsabellePlugin.depend.0 = jdk 1.5 -plugin.isabelle.jedit.IsabellePlugin.depend.1 = jedit 04.03.00.00 -plugin.isabelle.jedit.IsabellePlugin.depend.2 = plugin errorlist.ErrorListPlugin 1.7 -plugin.isabelle.jedit.IsabellePlugin.depend.3 = plugin sidekick.SideKickPlugin 0.7.4 - -#dockable component -isabelle.label = Isabelle -isabelle.title = Isabelle -isabelle.longtitle = Basic Isabelle process - -#menu -plugin.isabelle.jedit.IsabellePlugin.menu-item = isabelle - - -#Isabelle options -isabelle.print-modes = no_brackets no_type_brackets xsymbols -isabelle.logic = diff -r 0c5d1485dea7 -r 8d43e5e0588d lib/jedit/plugin/dockables.xml --- a/lib/jedit/plugin/dockables.xml Sat Nov 14 17:49:29 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,10 +0,0 @@ - - - - - - - new isabelle.jedit.IsabelleDock(view, position); - - - diff -r 0c5d1485dea7 -r 8d43e5e0588d lib/jedit/plugin/isabelle_dock.scala --- a/lib/jedit/plugin/isabelle_dock.scala Sat Nov 14 17:49:29 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,151 +0,0 @@ -/* Title: lib/jedit/plugin/isabelle_dock.scala - ID: $Id$ - Author: Makarius - -Dockable window for Isabelle process control. -*/ - -package isabelle.jedit - -import org.gjt.sp.jedit.View -import org.gjt.sp.jedit.gui.DefaultFocusComponent -import org.gjt.sp.jedit.gui.DockableWindowManager -import org.gjt.sp.jedit.gui.RolloverButton -import org.gjt.sp.jedit.gui.HistoryTextField -import org.gjt.sp.jedit.GUIUtilities - -import java.awt.Color -import java.awt.Insets -import java.awt.BorderLayout -import java.awt.Dimension -import java.awt.event.ActionListener -import java.awt.event.ActionEvent -import javax.swing.BoxLayout -import javax.swing.JPanel -import javax.swing.JScrollPane -import javax.swing.JTextPane -import javax.swing.text.{StyledDocument, StyleConstants} -import javax.swing.SwingUtilities -import javax.swing.Icon -import javax.swing.Box -import javax.swing.JTextField -import javax.swing.JComboBox -import javax.swing.DefaultComboBoxModel - - -class IsabelleDock(view: View, position: String) - extends JPanel(new BorderLayout) with DefaultFocusComponent -{ - private val text = new HistoryTextField("isabelle", false, true) - private val logic_combo = new JComboBox - - { - // output pane - val pane = new JTextPane - pane.setEditable(false) - add(BorderLayout.CENTER, new JScrollPane(pane)) - if (position == DockableWindowManager.FLOATING) - setPreferredSize(new Dimension(1000, 500)) - - val doc = pane.getDocument.asInstanceOf[StyledDocument] - - def make_style(name: String, bg: Boolean, color: Color) = { - val style = doc.addStyle(name, null) - if (bg) StyleConstants.setBackground(style, color) - else StyleConstants.setForeground(style, color) - style - } - val raw_style = make_style("raw", false, Color.GRAY) - val info_style = make_style("info", true, new Color(160, 255, 160)) - val warning_style = make_style("warning", true, new Color(255, 255, 160)) - val error_style = make_style("error", true, new Color(255, 160, 160)) - - IsabellePlugin.add_permanent_consumer (result => - if (result != null && !result.is_system) { - SwingUtilities.invokeLater(new Runnable { - def run = { - val logic = IsabellePlugin.isabelle.session - logic_combo.setModel(new DefaultComboBoxModel(Array(logic).asInstanceOf[Array[AnyRef]])) - logic_combo.setPrototypeDisplayValue("AAAA") // FIXME ?? - - val doc = pane.getDocument.asInstanceOf[StyledDocument] - val style = result.kind match { - case IsabelleProcess.Kind.WARNING => warning_style - case IsabelleProcess.Kind.ERROR => error_style - case IsabelleProcess.Kind.TRACING => info_style - case _ => if (result.is_raw) raw_style else null - } - doc.insertString(doc.getLength, IsabellePlugin.result_content(result), style) - if (!result.is_raw) doc.insertString(doc.getLength, "\n", style) - pane.setCaretPosition(doc.getLength) - } - }) - }) - - - // control box - val box = new Box(BoxLayout.X_AXIS) - add(BorderLayout.SOUTH, box) - - - // logic combo - logic_combo.setToolTipText("Isabelle logics") - logic_combo.setRequestFocusEnabled(false) - logic_combo.setModel(new DefaultComboBoxModel(Array("default").asInstanceOf[Array[AnyRef]])) - box.add(logic_combo) - - - // mode combo - val mode_Isar = "Isar" - val mode_ML = "ML" - val modes = Array(mode_Isar, mode_ML) - var mode = mode_Isar - - val mode_combo = new JComboBox - mode_combo.setToolTipText("Toplevel mode") - mode_combo.setRequestFocusEnabled(false) - mode_combo.setModel(new DefaultComboBoxModel(modes.asInstanceOf[Array[AnyRef]])) - mode_combo.setPrototypeDisplayValue("AAAA") - mode_combo.addActionListener(new ActionListener { - def actionPerformed(evt: ActionEvent): Unit = { - mode = mode_combo.getSelectedItem.asInstanceOf[String] - } - }) - box.add(mode_combo) - - - // input field - text.setToolTipText("Command line") - text.addActionListener(new ActionListener { - def actionPerformed(evt: ActionEvent): Unit = { - val command = IsabellePlugin.symbols.encode(text.getText) - if (command.length > 0) { - if (mode == mode_Isar) - IsabellePlugin.isabelle.command(command) - else if (mode == mode_ML) - IsabellePlugin.isabelle.ML(command) - text.setText("") - } - } - }) - box.add(text) - - - // buttons - def icon_button(icon: String, tip: String, action: => Unit) = { - val button = new RolloverButton(GUIUtilities.loadIcon(icon)) - button.setToolTipText(tip) - button.setMargin(new Insets(0,0,0,0)) - button.setRequestFocusEnabled(false) - button.addActionListener(new ActionListener { - def actionPerformed(evt: ActionEvent): Unit = action - }) - box.add(button) - } - - icon_button("Cancel.png", "Stop", IsabellePlugin.isabelle.interrupt) - icon_button("Clear.png", "Clear", pane.setText("")) - } - - def focusOnDefaultComponent: Unit = text.requestFocus -} diff -r 0c5d1485dea7 -r 8d43e5e0588d lib/jedit/plugin/isabelle_parser.scala --- a/lib/jedit/plugin/isabelle_parser.scala Sat Nov 14 17:49:29 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,72 +0,0 @@ -/* Title: lib/jedit/plugin/isabelle_parser.scala - ID: $Id$ - Author: Makarius - -Isabelle parser setup for Sidekick plugin. -*/ - -package isabelle.jedit - -import javax.swing.text.Position -import javax.swing.tree.DefaultMutableTreeNode -import javax.swing.tree.DefaultTreeModel - -import org.gjt.sp.jedit.{Buffer, EditPane} -import org.gjt.sp.util.Log - -import errorlist.DefaultErrorSource -import sidekick.{Asset, SideKickParser, SideKickParsedData, SideKickCompletion} - - -private class IsabelleAsset(name: String, content: String) extends Asset(name) -{ - override def getShortString() = { name } - override def getLongString() = { content } - override def getIcon() = { null } -} - - -class IsabelleParser extends SideKickParser("isabelle") { - - /* parsing */ - - private var stopped = false - - override def stop () { stopped = true } - - def parse(buffer: Buffer, e: DefaultErrorSource): SideKickParsedData = { - stopped = false - - var text: String = null - var data: SideKickParsedData = null - - try { - buffer.readLock() - text = buffer.getText(0, buffer.getLength) - data = new SideKickParsedData(buffer.getName) - - val asset = new IsabelleAsset("theory", null) - asset.setStart(buffer.createPosition(0)) - asset.setEnd(buffer.createPosition(buffer.getLength)) - - val node = new DefaultMutableTreeNode(asset) - data.root.insert(node, node.getChildCount) - - } - finally { - buffer.readUnlock() - } - - data - } - - - /* completion */ - - override def supportsCompletion = true - override def canCompleteAnywhere = true - - override def complete(pane: EditPane, caret: Int): SideKickCompletion = null - -} - diff -r 0c5d1485dea7 -r 8d43e5e0588d lib/jedit/plugin/isabelle_plugin.scala --- a/lib/jedit/plugin/isabelle_plugin.scala Sat Nov 14 17:49:29 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,170 +0,0 @@ -/* Title: lib/jedit/plugin/isabelle_plugin.scala - ID: $Id$ - Author: Makarius - -Isabelle/jEdit plugin -- main setup. -*/ - -package isabelle.jedit - -import java.util.Properties -import java.lang.NumberFormatException - -import scala.collection.mutable.ListBuffer -import scala.io.Source - -import org.gjt.sp.util.Log -import org.gjt.sp.jedit.{jEdit, EBPlugin, EBMessage} -import org.gjt.sp.jedit.msg.DockableWindowUpdate - -import errorlist.DefaultErrorSource -import errorlist.ErrorSource - - - -/** global state **/ - -object IsabellePlugin { - - /* Isabelle symbols */ - - val symbols = new Symbol.Interpretation - - def result_content(result: IsabelleProcess.Result) = - XML.content(YXML.parse_failsafe(symbols.decode(result.result))).mkString("") - - - /* Isabelle process */ - - var isabelle: IsabelleProcess = null - - - /* unique ids */ - - private var id_count: BigInt = 0 - - def id() : String = synchronized { id_count += 1; "jedit:" + id_count } - - def id_properties(value: String) : Properties = { - val props = new Properties - props.setProperty(Markup.ID, value) - props - } - - def id_properties() : Properties = { id_properties(id()) } - - - /* result consumers */ - - type Consumer = IsabelleProcess.Result => Boolean - private var consumers = new ListBuffer[Consumer] - - def add_consumer(consumer: Consumer) = synchronized { consumers += consumer } - - def add_permanent_consumer(consumer: IsabelleProcess.Result => Unit) = { - add_consumer(result => { consumer(result); false }) - } - - def del_consumer(consumer: Consumer) = synchronized { consumers -= consumer } - - private def consume(result: IsabelleProcess.Result) = { - synchronized { consumers.elements.toList } foreach (consumer => - { - if (result != null && result.is_control) Log.log(Log.DEBUG, result, null) - val finished = - try { consumer(result) } - catch { case e: Throwable => Log.log(Log.ERROR, result, e); true } - if (finished || result == null) del_consumer(consumer) - }) - } - - class ConsumerThread extends Thread { - override def run = { - var finished = false - while (!finished) { - val result = - try { IsabellePlugin.isabelle.get_result() } - catch { case _: NullPointerException => null } - - if (result != null) { - consume(result) - if (result.kind == IsabelleProcess.Kind.EXIT) { - consume(null) - finished = true - } - } - else finished = true - } - } - } - -} - - -/* Main plugin setup */ - -class IsabellePlugin extends EBPlugin { - - import IsabellePlugin._ - - val errors = new DefaultErrorSource("isabelle") - val consumer_thread = new ConsumerThread - - - override def start = { - - /* error source */ - - ErrorSource.registerErrorSource(errors) - - add_permanent_consumer (result => - if (result != null && - (result.kind == IsabelleProcess.Kind.WARNING || - result.kind == IsabelleProcess.Kind.ERROR)) { - (Position.line_of(result.props), Position.file_of(result.props)) match { - case (Some(line), Some(file)) => - val typ = - if (result.kind == IsabelleProcess.Kind.WARNING) ErrorSource.WARNING - else ErrorSource.ERROR - val content = result_content(result) - if (content.length > 0) { - val lines = Source.fromString(content).getLines - val err = new DefaultErrorSource.DefaultError(errors, - typ, file, line - 1, 0, 0, lines.next) - for (msg <- lines) err.addExtraMessage(msg) - errors.addError(err) - } - case _ => - } - }) - - - /* Isabelle process */ - - val options = - (for (mode <- jEdit.getProperty("isabelle.print-modes").split("\\s+") if mode != "") - yield "-m" + mode) - val args = { - val logic = jEdit.getProperty("isabelle.logic") - if (logic != "") List(logic) else Nil - } - isabelle = new IsabelleProcess((options ++ args): _*) - - consumer_thread.start - - } - - - override def stop = { - isabelle.kill - consumer_thread.join - ErrorSource.unregisterErrorSource(errors) - } - - - override def handleMessage(message: EBMessage) = message match { - case _: DockableWindowUpdate => // FIXME check isabelle process - case _ => - } - -} diff -r 0c5d1485dea7 -r 8d43e5e0588d lib/jedit/plugin/mk --- a/lib/jedit/plugin/mk Sat Nov 14 17:49:29 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,22 +0,0 @@ -#!/bin/bash -# $Id$ - -JEDIT_HOME="$HOME/lib/jedit/current" -PLUGINS="$HOME/.jedit/jars" - - -rm -rf build/ && mkdir -p build -rm -f ../isabelle.jar - -scalac -d build \ - -cp $JEDIT_HOME/jedit.jar:$PLUGINS/SideKick.jar:$PLUGINS/ErrorList.jar:$PLUGINS/Console.jar:../../classes/Pure.jar \ - isabelle_plugin.scala \ - isabelle_dock.scala \ - isabelle_parser.scala \ -&& ( - cp *.xml *.props build/ - cd build - jar cf ../../isabelle.jar . -) - -rm -rf build/ diff -r 0c5d1485dea7 -r 8d43e5e0588d lib/jedit/plugin/services.xml --- a/lib/jedit/plugin/services.xml Sat Nov 14 17:49:29 2009 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,10 +0,0 @@ - - - - - - - new isabelle.jedit.IsabelleParser(); - - -