--- 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
-
- <MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>
-
-Example catalog file:
-
- <?xml version="1.0"?>
- <!DOCTYPE MODES SYSTEM "catalog.dtd">
- <MODES>
- <MODE NAME="isabelle" FILE="isabelle.xml" FILE_NAME_GLOB="*.thy"/>
- </MODES>
-
-
-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$
--- 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 @@
-<?xml version="1.0"?>
-<!DOCTYPE MODE SYSTEM "xmode.dtd">
-<!-- Generated from Pure + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace + FOL + ZF. -->
-<!-- *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** -->
-<MODE>
- <PROPS>
- <PROPERTY NAME="commentStart" VALUE="(*"/>
- <PROPERTY NAME="commentEnd" VALUE="*)"/>
- <PROPERTY NAME="noWordSep" VALUE="_'.?"/>
- <PROPERTY NAME="indentOpenBrackets" VALUE="{"/>
- <PROPERTY NAME="indentCloseBrackets" VALUE="}"/>
- <PROPERTY NAME="unalignedOpenBrackets" VALUE="(" />
- <PROPERTY NAME="unalignedCloseBrackets" VALUE=")" />
- <PROPERTY NAME="tabSize" VALUE="2" />
- <PROPERTY NAME="indentSize" VALUE="2" />
- </PROPS>
- <RULES IGNORE_CASE="FALSE" HIGHLIGHT_DIGITS="FALSE" ESCAPE="\">
- <SPAN TYPE="COMMENT1" NO_ESCAPE="TRUE">
- <BEGIN>(*</BEGIN>
- <END>*)</END>
- </SPAN>
- <SPAN TYPE="COMMENT3" NO_ESCAPE="TRUE">
- <BEGIN>{*</BEGIN>
- <END>*}</END>
- </SPAN>
- <SPAN TYPE="LITERAL1">
- <BEGIN>`</BEGIN>
- <END>`</END>
- </SPAN>
- <SPAN TYPE="LITERAL3">
- <BEGIN>"</BEGIN>
- <END>"</END>
- </SPAN>
- <KEYWORDS>
- <OPERATOR>.</OPERATOR>
- <OPERATOR>..</OPERATOR>
- <INVALID>Isabelle.command</INVALID>
- <INVALID>Isar.begin_document</INVALID>
- <INVALID>Isar.define_command</INVALID>
- <INVALID>Isar.edit_document</INVALID>
- <INVALID>Isar.end_document</INVALID>
- <OPERATOR>ML</OPERATOR>
- <LABEL>ML_command</LABEL>
- <OPERATOR>ML_prf</OPERATOR>
- <LABEL>ML_val</LABEL>
- <OPERATOR>abbreviation</OPERATOR>
- <KEYWORD4>actions</KEYWORD4>
- <KEYWORD4>advanced</KEYWORD4>
- <OPERATOR>also</OPERATOR>
- <KEYWORD4>and</KEYWORD4>
- <KEYWORD1>apply</KEYWORD1>
- <KEYWORD1>apply_end</KEYWORD1>
- <OPERATOR>arities</OPERATOR>
- <KEYWORD2>assume</KEYWORD2>
- <KEYWORD4>assumes</KEYWORD4>
- <OPERATOR>atom_decl</OPERATOR>
- <LABEL>atp_info</LABEL>
- <LABEL>atp_kill</LABEL>
- <LABEL>atp_messages</LABEL>
- <LABEL>atp_minimize</LABEL>
- <KEYWORD4>attach</KEYWORD4>
- <OPERATOR>attribute_setup</OPERATOR>
- <OPERATOR>automaton</OPERATOR>
- <KEYWORD4>avoids</KEYWORD4>
- <OPERATOR>ax_specification</OPERATOR>
- <OPERATOR>axclass</OPERATOR>
- <OPERATOR>axiomatization</OPERATOR>
- <OPERATOR>axioms</OPERATOR>
- <KEYWORD1>back</KEYWORD1>
- <KEYWORD4>begin</KEYWORD4>
- <KEYWORD4>binder</KEYWORD4>
- <OPERATOR>by</OPERATOR>
- <INVALID>cannot_undo</INVALID>
- <KEYWORD2>case</KEYWORD2>
- <KEYWORD4>case_eqns</KEYWORD4>
- <LABEL>cd</LABEL>
- <OPERATOR>chapter</OPERATOR>
- <OPERATOR>class</OPERATOR>
- <LABEL>class_deps</LABEL>
- <OPERATOR>classes</OPERATOR>
- <OPERATOR>classrel</OPERATOR>
- <OPERATOR>codatatype</OPERATOR>
- <OPERATOR>code_abort</OPERATOR>
- <OPERATOR>code_class</OPERATOR>
- <OPERATOR>code_const</OPERATOR>
- <OPERATOR>code_datatype</OPERATOR>
- <LABEL>code_deps</LABEL>
- <OPERATOR>code_include</OPERATOR>
- <OPERATOR>code_instance</OPERATOR>
- <OPERATOR>code_library</OPERATOR>
- <OPERATOR>code_module</OPERATOR>
- <OPERATOR>code_modulename</OPERATOR>
- <OPERATOR>code_monad</OPERATOR>
- <OPERATOR>code_pred</OPERATOR>
- <OPERATOR>code_reserved</OPERATOR>
- <LABEL>code_thms</LABEL>
- <OPERATOR>code_type</OPERATOR>
- <OPERATOR>coinductive</OPERATOR>
- <OPERATOR>coinductive_set</OPERATOR>
- <LABEL>commit</LABEL>
- <KEYWORD4>compose</KEYWORD4>
- <KEYWORD4>con_defs</KEYWORD4>
- <KEYWORD4>congs</KEYWORD4>
- <OPERATOR>constdefs</OPERATOR>
- <KEYWORD4>constrains</KEYWORD4>
- <OPERATOR>consts</OPERATOR>
- <OPERATOR>consts_code</OPERATOR>
- <KEYWORD4>contains</KEYWORD4>
- <OPERATOR>context</OPERATOR>
- <OPERATOR>corollary</OPERATOR>
- <OPERATOR>cpodef</OPERATOR>
- <OPERATOR>datatype</OPERATOR>
- <OPERATOR>declaration</OPERATOR>
- <OPERATOR>declare</OPERATOR>
- <KEYWORD2>def</KEYWORD2>
- <OPERATOR>defaultsort</OPERATOR>
- <KEYWORD1>defer</KEYWORD1>
- <OPERATOR>defer_recdef</OPERATOR>
- <KEYWORD4>defines</KEYWORD4>
- <OPERATOR>definition</OPERATOR>
- <OPERATOR>defs</OPERATOR>
- <LABEL>disable_pr</LABEL>
- <LABEL>display_drafts</LABEL>
- <OPERATOR>domain</OPERATOR>
- <KEYWORD4>domains</KEYWORD4>
- <OPERATOR>done</OPERATOR>
- <KEYWORD4>elimination</KEYWORD4>
- <LABEL>enable_pr</LABEL>
- <KEYWORD3>end</KEYWORD3>
- <OPERATOR>equivariance</OPERATOR>
- <INVALID>exit</INVALID>
- <LABEL>export_code</LABEL>
- <OPERATOR>extract</OPERATOR>
- <OPERATOR>extract_type</OPERATOR>
- <KEYWORD4>file</KEYWORD4>
- <OPERATOR>finalconsts</OPERATOR>
- <OPERATOR>finally</OPERATOR>
- <LABEL>find_consts</LABEL>
- <LABEL>find_theorems</LABEL>
- <KEYWORD2>fix</KEYWORD2>
- <KEYWORD4>fixes</KEYWORD4>
- <OPERATOR>fixpat</OPERATOR>
- <OPERATOR>fixrec</OPERATOR>
- <KEYWORD4>for</KEYWORD4>
- <OPERATOR>from</OPERATOR>
- <LABEL>full_prf</LABEL>
- <OPERATOR>fun</OPERATOR>
- <OPERATOR>function</OPERATOR>
- <OPERATOR>global</OPERATOR>
- <KEYWORD2>guess</KEYWORD2>
- <OPERATOR>have</OPERATOR>
- <LABEL>header</LABEL>
- <LABEL>help</LABEL>
- <OPERATOR>hence</OPERATOR>
- <OPERATOR>hide</OPERATOR>
- <KEYWORD4>hide_action</KEYWORD4>
- <KEYWORD4>hints</KEYWORD4>
- <KEYWORD4>identifier</KEYWORD4>
- <KEYWORD4>if</KEYWORD4>
- <KEYWORD4>imports</KEYWORD4>
- <KEYWORD4>in</KEYWORD4>
- <KEYWORD4>induction</KEYWORD4>
- <OPERATOR>inductive</OPERATOR>
- <KEYWORD1>inductive_cases</KEYWORD1>
- <OPERATOR>inductive_set</OPERATOR>
- <KEYWORD4>infix</KEYWORD4>
- <KEYWORD4>infixl</KEYWORD4>
- <KEYWORD4>infixr</KEYWORD4>
- <INVALID>init_toplevel</INVALID>
- <KEYWORD4>initially</KEYWORD4>
- <KEYWORD4>inputs</KEYWORD4>
- <OPERATOR>instance</OPERATOR>
- <OPERATOR>instantiation</OPERATOR>
- <KEYWORD4>internals</KEYWORD4>
- <OPERATOR>interpret</OPERATOR>
- <OPERATOR>interpretation</OPERATOR>
- <KEYWORD4>intros</KEYWORD4>
- <KEYWORD4>is</KEYWORD4>
- <OPERATOR>judgment</OPERATOR>
- <INVALID>kill</INVALID>
- <LABEL>kill_thy</LABEL>
- <KEYWORD4>lazy</KEYWORD4>
- <OPERATOR>lemma</OPERATOR>
- <OPERATOR>lemmas</OPERATOR>
- <OPERATOR>let</OPERATOR>
- <INVALID>linear_undo</INVALID>
- <OPERATOR>local</OPERATOR>
- <OPERATOR>local_setup</OPERATOR>
- <OPERATOR>locale</OPERATOR>
- <OPERATOR>method_setup</OPERATOR>
- <KEYWORD4>module_name</KEYWORD4>
- <KEYWORD4>monos</KEYWORD4>
- <OPERATOR>moreover</OPERATOR>
- <KEYWORD4>morphisms</KEYWORD4>
- <OPERATOR>next</OPERATOR>
- <LABEL>nitpick</LABEL>
- <OPERATOR>nitpick_params</OPERATOR>
- <OPERATOR>no_notation</OPERATOR>
- <OPERATOR>no_syntax</OPERATOR>
- <OPERATOR>no_translations</OPERATOR>
- <OPERATOR>nominal_datatype</OPERATOR>
- <OPERATOR>nominal_inductive</OPERATOR>
- <OPERATOR>nominal_inductive2</OPERATOR>
- <OPERATOR>nominal_primrec</OPERATOR>
- <OPERATOR>nonterminals</OPERATOR>
- <LABEL>normal_form</LABEL>
- <OPERATOR>notation</OPERATOR>
- <OPERATOR>note</OPERATOR>
- <KEYWORD4>notes</KEYWORD4>
- <KEYWORD2>obtain</KEYWORD2>
- <KEYWORD4>obtains</KEYWORD4>
- <OPERATOR>oops</OPERATOR>
- <KEYWORD4>open</KEYWORD4>
- <OPERATOR>oracle</OPERATOR>
- <KEYWORD4>output</KEYWORD4>
- <KEYWORD4>outputs</KEYWORD4>
- <KEYWORD4>overloaded</KEYWORD4>
- <OPERATOR>overloading</OPERATOR>
- <OPERATOR>parse_ast_translation</OPERATOR>
- <OPERATOR>parse_translation</OPERATOR>
- <OPERATOR>pcpodef</OPERATOR>
- <KEYWORD4>permissive</KEYWORD4>
- <KEYWORD4>post</KEYWORD4>
- <LABEL>pr</LABEL>
- <KEYWORD4>pre</KEYWORD4>
- <KEYWORD1>prefer</KEYWORD1>
- <KEYWORD2>presume</KEYWORD2>
- <LABEL>pretty_setmargin</LABEL>
- <LABEL>prf</LABEL>
- <OPERATOR>primrec</OPERATOR>
- <LABEL>print_abbrevs</LABEL>
- <LABEL>print_antiquotations</LABEL>
- <OPERATOR>print_ast_translation</OPERATOR>
- <LABEL>print_atps</LABEL>
- <LABEL>print_attributes</LABEL>
- <LABEL>print_binds</LABEL>
- <LABEL>print_cases</LABEL>
- <LABEL>print_claset</LABEL>
- <LABEL>print_classes</LABEL>
- <LABEL>print_codeproc</LABEL>
- <LABEL>print_codesetup</LABEL>
- <LABEL>print_commands</LABEL>
- <LABEL>print_configs</LABEL>
- <LABEL>print_context</LABEL>
- <LABEL>print_drafts</LABEL>
- <LABEL>print_facts</LABEL>
- <LABEL>print_induct_rules</LABEL>
- <LABEL>print_interps</LABEL>
- <LABEL>print_locale</LABEL>
- <LABEL>print_locales</LABEL>
- <LABEL>print_methods</LABEL>
- <LABEL>print_orders</LABEL>
- <LABEL>print_rules</LABEL>
- <LABEL>print_simpset</LABEL>
- <LABEL>print_statement</LABEL>
- <LABEL>print_syntax</LABEL>
- <LABEL>print_tcset</LABEL>
- <LABEL>print_theorems</LABEL>
- <LABEL>print_theory</LABEL>
- <LABEL>print_trans_rules</LABEL>
- <OPERATOR>print_translation</OPERATOR>
- <OPERATOR>proof</OPERATOR>
- <LABEL>prop</LABEL>
- <LABEL>pwd</LABEL>
- <OPERATOR>qed</OPERATOR>
- <LABEL>quickcheck</LABEL>
- <OPERATOR>quickcheck_params</OPERATOR>
- <INVALID>quit</INVALID>
- <OPERATOR>realizability</OPERATOR>
- <OPERATOR>realizers</OPERATOR>
- <OPERATOR>recdef</OPERATOR>
- <OPERATOR>recdef_tc</OPERATOR>
- <OPERATOR>record</OPERATOR>
- <KEYWORD4>recursor_eqns</KEYWORD4>
- <LABEL>refute</LABEL>
- <OPERATOR>refute_params</OPERATOR>
- <LABEL>remove_thy</LABEL>
- <KEYWORD4>rename</KEYWORD4>
- <OPERATOR>rep_datatype</OPERATOR>
- <KEYWORD4>restrict</KEYWORD4>
- <OPERATOR>sect</OPERATOR>
- <OPERATOR>section</OPERATOR>
- <OPERATOR>setup</OPERATOR>
- <KEYWORD2>show</KEYWORD2>
- <KEYWORD4>shows</KEYWORD4>
- <KEYWORD4>signature</KEYWORD4>
- <OPERATOR>simproc_setup</OPERATOR>
- <LABEL>sledgehammer</LABEL>
- <OPERATOR>sorry</OPERATOR>
- <OPERATOR>specification</OPERATOR>
- <KEYWORD4>states</KEYWORD4>
- <OPERATOR>statespace</OPERATOR>
- <KEYWORD4>structure</KEYWORD4>
- <OPERATOR>subclass</OPERATOR>
- <OPERATOR>sublocale</OPERATOR>
- <OPERATOR>subsect</OPERATOR>
- <OPERATOR>subsection</OPERATOR>
- <OPERATOR>subsubsect</OPERATOR>
- <OPERATOR>subsubsection</OPERATOR>
- <OPERATOR>syntax</OPERATOR>
- <LABEL>term</LABEL>
- <OPERATOR>termination</OPERATOR>
- <OPERATOR>text</OPERATOR>
- <OPERATOR>text_raw</OPERATOR>
- <OPERATOR>then</OPERATOR>
- <OPERATOR>theorem</OPERATOR>
- <OPERATOR>theorems</OPERATOR>
- <KEYWORD3>theory</KEYWORD3>
- <LABEL>thm</LABEL>
- <LABEL>thm_deps</LABEL>
- <KEYWORD2>thus</KEYWORD2>
- <LABEL>thy_deps</LABEL>
- <KEYWORD4>to</KEYWORD4>
- <LABEL>touch_thy</LABEL>
- <KEYWORD4>transitions</KEYWORD4>
- <OPERATOR>translations</OPERATOR>
- <KEYWORD4>transrel</KEYWORD4>
- <OPERATOR>txt</OPERATOR>
- <OPERATOR>txt_raw</OPERATOR>
- <LABEL>typ</LABEL>
- <KEYWORD4>type_elims</KEYWORD4>
- <KEYWORD4>type_intros</KEYWORD4>
- <OPERATOR>typed_print_translation</OPERATOR>
- <OPERATOR>typedecl</OPERATOR>
- <OPERATOR>typedef</OPERATOR>
- <OPERATOR>types</OPERATOR>
- <OPERATOR>types_code</OPERATOR>
- <OPERATOR>ultimately</OPERATOR>
- <KEYWORD4>unchecked</KEYWORD4>
- <INVALID>undo</INVALID>
- <INVALID>undos_proof</INVALID>
- <OPERATOR>unfolding</OPERATOR>
- <LABEL>unused_thms</LABEL>
- <OPERATOR>use</OPERATOR>
- <LABEL>use_thy</LABEL>
- <KEYWORD4>uses</KEYWORD4>
- <OPERATOR>using</OPERATOR>
- <LABEL>value</LABEL>
- <LABEL>values</LABEL>
- <LABEL>welcome</LABEL>
- <KEYWORD4>where</KEYWORD4>
- <OPERATOR>with</OPERATOR>
- <OPERATOR>{</OPERATOR>
- <OPERATOR>}</OPERATOR>
- </KEYWORDS>
- </RULES>
-</MODE>
--- 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 =
--- 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 @@
-<?xml version="1.0"?>
-<!DOCTYPE DOCKABLES SYSTEM "dockables.dtd">
-<!-- $Id$ -->
-
-<DOCKABLES>
- <DOCKABLE NAME="isabelle" MOVABLE="TRUE">
- new isabelle.jedit.IsabelleDock(view, position);
- </DOCKABLE>
-</DOCKABLES>
-
--- 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
-}
--- 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
-
-}
-
--- 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 _ =>
- }
-
-}
--- 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/
--- 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 @@
-<?xml version="1.0"?>
-<!DOCTYPE SERVICES SYSTEM "services.dtd">
-<!-- $Id$ -->
-
-<SERVICES>
- <SERVICE CLASS="sidekick.SideKickParser" NAME="isabelle">
- new isabelle.jedit.IsabelleParser();
- </SERVICE>
-</SERVICES>
-