--- a/src/Pure/Tools/main.scala Sat Sep 21 16:08:17 2013 +0200
+++ b/src/Pure/Tools/main.scala Sat Sep 21 16:44:31 2013 +0200
@@ -82,7 +82,7 @@
if (!(settings_dir + Path.explode("perspective.xml")).is_file) {
File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"),
- """<DOCKING LEFT="" TOP="" RIGHT="" BOTTOM="isabelle-readme" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""")
+ """<DOCKING LEFT="" TOP="" RIGHT="isabelle-documentation" BOTTOM="" LEFT_POS="0" TOP_POS="0" RIGHT_POS="250" BOTTOM_POS="250" />""")
File.write(settings_dir + Path.explode("perspective.xml"),
"""<?xml version="1.0" encoding="UTF-8" ?>
<!DOCTYPE PERSPECTIVE SYSTEM "perspective.dtd">
--- a/src/Tools/jEdit/README.html Sat Sep 21 16:08:17 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,237 +0,0 @@
-<?xml version="1.0" encoding="UTF-8" ?>
-<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Transitional//EN" "http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd">
-<html xmlns="http://www.w3.org/1999/xhtml">
-
-<head>
-<meta http-equiv="Content-Type" content="text/html; charset=utf-8"/>
-<style type="text/css" media="screen">
-body { font-family: IsabelleText; font-size: 14pt; }
-</style>
-<title>Welcome to the Isabelle/jEdit Prover IDE</title>
-</head>
-
-<body>
-
-<center><h2><img alt="PIDE" src="PIDE.png" width="230" align="middle"/></h2></center>
-
-<p>
- <b>PIDE</b> is a framework for Prover IDEs based on the
- Isabelle/Scala. It is built around a concept of
- <em>asynchronous document processing</em>, which is supported
- natively by the <em>parallel proof engine</em> that is implemented
- in Isabelle/ML.
-</p>
-
-<p>
- <b>Isabelle/jEdit</b> is the main example application of the PIDE
- framework — it is ready for small and large Isabelle
- applications, for beginners and experts alike.
-</p>
-
-<p>
- <em>Research and implementation of concepts around PIDE has started
- around 2008 and was kindly supported by BMBF (http://www.bmbf.de),
- Université Paris-Sud (http://www.u-psud.fr), Digiteo
- (http://www.digiteo.fr), and ANR
- (http://www.agence-nationale-recherche.fr).</em>
-</p>
-
-
-
-<h2>The Isabelle/jEdit Prover IDE</h2>
-
-<p>
-Isabelle/jEdit consists of some plugins for the well-known jEdit text
-editor framework (http://www.jedit.org), according to the following
-principles.
-</p>
-
-<ul>
-
-<li>The original jEdit look-and-feel is generally preserved, although some
-default properties have been changed to accommodate Isabelle (e.g. the text
-area font).</li>
-
-<li>Formal Isabelle/Isar text is checked asynchronously while editing. The
-user is in full command of the editor, and the prover refrains from locking
-portions of the buffer.</li>
-
-<li>Prover feedback works via colors, boxes, squiggly underline,
-hyperlinks, popup windows, icons, clickable output, all based on semantic
-markup produced by Isabelle in the background.</li>
-
-<li>Using the mouse together with the modifier key <tt>CONTROL</tt> (Linux,
-Windows) or <tt>COMMAND</tt> (Mac OS X) exposes additional formal
-content.</li>
-
-<li>Dockable panels (e.g. <em>Output</em>, <em>Symbols</em>) are managed as
-independent windows by jEdit, which also allows multiple instances.</li>
-
-<li>Formal output (in popups etc.) may be explored recursively, using the
-same techniques as in the editor source buffer.</li>
-
-<li>The prover process and source files are managed on the editor side. The
-prover operates on timeless and stateless document content via
-Isabelle/Scala.</li>
-
-<li>Plugin options of jEdit (for the <em>Isabelle</em> plugin) give access
-to a selection of Isabelle/Scala options and its persistence preferences,
-usually with immediate effect on the prover back-end or editor
-front-end.</li>
-
-<li>The logic image of the prover session may be specified within
-Isabelle/jEdit, but this requires restart. The new image is provided
-automatically by the Isabelle build process.</li>
-
-</ul>
-
-
-<h2>Isabelle symbols and fonts</h2>
-
-<ul>
- <li>Isabelle supports infinitely many symbols:<br/>
- α, β, γ, …<br/>
- ∀, ∃, ∨, ∧, ⟶, ⟷, …<br/>
- ≤, ≥, ⊓, ⊔, …<br/>
- ℵ, △, ∇, …<br/>
- <tt>\<foo></tt>, <tt>\<bar></tt>, <tt>\<baz></tt>, …<br/>
- </li>
-
- <li>There are some special control symbols to modify the style of a
- <em>single</em> symbol:<br/>
- ⇩ subscript<br/>
- ⇧ superscript<br/>
- ⇣ subscript within identifier<br/>
- ⇡ superscript within identifier<br/>
- ❙ bold face</li>
-
- <li>A default mapping relates some Isabelle symbols to Unicode points
- (see <tt>$ISABELLE_HOME/etc/symbols</tt> and <tt>$ISABELLE_HOME_USER/etc/symbols</tt>).
- </li>
-
- <li>The <em>IsabelleText</em> font ensures that Unicode points are actually
- seen on the screen (or printer).
- </li>
-
- <li>Input methods:
- <ul>
- <li>use the Symbols dockable</li>
- <li>copy/paste from decoded source files</li>
- <li>copy/paste from prover output</li>
- <li>completion provided by Isabelle plugin, e.g.<br/>
-
- <table border="1">
- <tr><th><b>name</b></th> <th><b>abbreviation</b></th> <th><b>symbol</b></th></tr>
-
- <tr><td>lambda</td> <td><tt>%</tt></td> <td>λ</td></tr>
- <tr><td>Rightarrow</td> <td><tt>=></tt></td> <td>⇒</td></tr>
- <tr><td>Longrightarrow</td> <td><tt>==></tt></td> <td>⟹</td></tr>
-
- <tr><td>And</td> <td><tt>!!</tt></td> <td>⋀</td></tr>
- <tr><td>equiv</td> <td><tt>==</tt></td> <td>≡</td></tr>
-
- <tr><td>forall</td> <td><tt>!</tt></td> <td>∀</td></tr>
- <tr><td>exists</td> <td><tt>?</tt></td> <td>∃</td></tr>
- <tr><td>longrightarrow</td> <td><tt>--></tt></td> <td>⟶</td></tr>
- <tr><td>and</td> <td><tt>/\</tt></td> <td>∧</td></tr>
- <tr><td>or</td> <td><tt>\/</tt></td> <td>∨</td></tr>
- <tr><td>not</td> <td><tt>~ </tt></td> <td>¬</td></tr>
- <tr><td>noteq</td> <td><tt>~=</tt></td> <td>≠</td></tr>
- <tr><td>in</td> <td><tt>:</tt></td> <td>∈</td></tr>
- <tr><td>notin</td> <td><tt>~:</tt></td> <td>∉</td></tr>
-
- <tr><td>sub</td> <td><tt>=_</tt></td> <td>⇩</td></tr>
- <tr><td>sup</td> <td><tt>=^</tt></td> <td>⇧</td></tr>
- <tr><td>bold</td> <td><tt>-.</tt></td> <td>❙</td></tr>
-
- </table>
- </li>
- </ul>
- </li>
-
- <li><b>NOTE:</b> The above abbreviations refer to the input method.
- The logical notation provides ASCII alternatives that often
- coincide, but deviate occasionally.
- </li>
-
- <li><b>NOTE:</b> Generic jEdit abbreviations or plugins perform similar
- source replacement operations; this works for Isabelle as long
- as the Unicode sequences coincide with the symbol mapping.
- </li>
-
- <li><b>NOTE:</b> Raw Unicode characters within prover source files
- should be restricted to informal parts, e.g. to write text in
- non-latin alphabets. Mathematical symbols should be defined via the
- official rendering tables.
- </li>
-
- <li><b>NOTE:</b> Control symbols may be applied to a region of selected
- text, either using the Symbols dockable or keyboard shortcuts.</li>
-
-</ul>
-
-
-<h2>Limitations and known problems</h2>
-
-<ul>
- <li>Keyboard shortcuts C-PLUS and C-MINUS for adjusting the editor font
- size depend on platform details and national keyboards.<br/>
- <em>Workaround: Use numeric keypad or rebind keys in the jEdit Shortcuts
- options dialog.</em></li>
-
- <li>Lack of dependency management for auxiliary files that contribute
- to a theory (e.g. <tt>ML_file</tt>).<br/>
- <em>Workaround:</em> Re-load files manually within the prover.</li>
-
- <li>Odd behavior of some diagnostic commands with global
- side-effects, like writing a physical
- file.<br/>
- <em>Workaround:</em> Avoid such commands.</li>
-
- <li>No way to delete document nodes from the overall collection of
- theories.<br/>
- <em>Workaround:</em> Restart whole Isabelle/jEdit session in
- worst-case situation.</li>
-
- <li>Linux: some desktop environments with extreme animation effects
- may disrupt Java 7 window placement and keyboard focus.<br/>
- <em>Workaround:</em> Disable such effects.</li>
-
- <li>Linux: some X11 window managers that are not "re-parenting"
- cause problems with additional windows opened by the Java VM. This
- affects either historic or neo-minimalistic window managers like
- <em>awesome</em> or <em>xmonad</em>.<br/>
- <em>Workaround:</em> Use regular re-parenting window manager.</li>
-
- <li>Mac OS X: the native MacOSX plugin for jEdit tends to be
- disruptive and is off by default. Enabling it might or might not
- improve the user experience.<br/>
- <em>Workaround:</em> Disable MacOSX plugin.</li></li>
-
- <li>Mac OS X: Java 7 is officially supported on Lion and Mountain Lion,
- but not Snow Leopard. It usually works on the latter, although with a
- small risk of instabilities.<br/>
- <em>Workaround:</em> Update to OS X Mountain Lion.</li>
-</ul>
-
-
-<h2>Licenses and home sites of contributing systems</h2>
-
-<ul>
-
-<li>Isabelle: BSD-style</li>
-
-<li>Poly/ML: LGPL <br/> http://www.polyml.org </li>
-
-<li>Scala: BSD-style <br/> http://www.scala-lang.org</li>
-
-<li>jEdit: GPL (with special cases) <br/> http://www.jedit.org</li>
-
-<li>JFreeChart: LGPL <br/> http://www.jfree.org</li>
-
-<li>Lobo/Cobra: GPL and LGPL <br/> http://lobobrowser.org</li>
-
-</ul>
-
-</body>
-</html>
--- a/src/Tools/jEdit/lib/Tools/jedit Sat Sep 21 16:08:17 2013 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit Sat Sep 21 16:44:31 2013 +0200
@@ -17,7 +17,6 @@
"src/find_dockable.scala"
"src/fold_handling.scala"
"src/graphview_dockable.scala"
- "src/html_panel.scala"
"src/info_dockable.scala"
"src/isabelle.scala"
"src/isabelle_encoding.scala"
@@ -38,7 +37,6 @@
"src/process_indicator.scala"
"src/protocol_dockable.scala"
"src/raw_output_dockable.scala"
- "src/readme_dockable.scala"
"src/rendering.scala"
"src/rich_text_area.scala"
"src/scala_console.scala"
--- a/src/Tools/jEdit/src/Isabelle.props Sat Sep 21 16:08:17 2013 +0200
+++ b/src/Tools/jEdit/src/Isabelle.props Sat Sep 21 16:44:31 2013 +0200
@@ -36,7 +36,6 @@
isabelle.output-panel \
isabelle.protocol-panel \
isabelle.raw-output-panel \
- isabelle.readme-panel \
isabelle.sledgehammer-panel \
isabelle.symbols-panel \
isabelle.syslog-panel \
@@ -48,7 +47,6 @@
isabelle.output-panel.label=Output panel
isabelle.protocol-panel.label=Protocol panel
isabelle.raw-output-panel.label=Raw Output panel
-isabelle.readme-panel.label=README panel
isabelle.sledgehammer-panel.label=Sledgehammer panel
isabelle.symbols-panel.label=Symbols panel
isabelle.syslog-panel.label=Syslog panel
@@ -64,7 +62,6 @@
isabelle-protocol.title=Protocol
isabelle-raw-output.title=Raw Output
isabelle-documentation.title=Documentation
-isabelle-readme.title=README
isabelle-sledgehammer.title=Sledgehammer
isabelle-symbols.title=Symbols
isabelle-syslog.title=Syslog
--- a/src/Tools/jEdit/src/actions.xml Sat Sep 21 16:08:17 2013 +0200
+++ b/src/Tools/jEdit/src/actions.xml Sat Sep 21 16:44:31 2013 +0200
@@ -22,11 +22,6 @@
wm.addDockableWindow("isabelle-documentation");
</CODE>
</ACTION>
- <ACTION NAME="isabelle.readme-panel">
- <CODE>
- wm.addDockableWindow("isabelle-readme");
- </CODE>
- </ACTION>
<ACTION NAME="isabelle.find-panel">
<CODE>
wm.addDockableWindow("isabelle-find");
--- a/src/Tools/jEdit/src/dockables.xml Sat Sep 21 16:08:17 2013 +0200
+++ b/src/Tools/jEdit/src/dockables.xml Sat Sep 21 16:44:31 2013 +0200
@@ -14,9 +14,6 @@
<DOCKABLE NAME="isabelle-documentation" MOVABLE="TRUE">
new isabelle.jedit.Documentation_Dockable(view, position);
</DOCKABLE>
- <DOCKABLE NAME="isabelle-readme" MOVABLE="TRUE">
- new isabelle.jedit.README_Dockable(view, position);
- </DOCKABLE>
<DOCKABLE NAME="isabelle-output" MOVABLE="TRUE">
new isabelle.jedit.Output_Dockable(view, position);
</DOCKABLE>
--- a/src/Tools/jEdit/src/html_panel.scala Sat Sep 21 16:08:17 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,36 +0,0 @@
-/* Title: Tools/jEdit/src/html_panel.scala
- Author: Makarius
-
-HTML panel based on Lobo/Cobra.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import java.io.StringReader
-
-import java.util.logging.{Logger, Level}
-
-import org.lobobrowser.html.parser.{DocumentBuilderImpl, InputSourceImpl}
-import org.lobobrowser.html.gui.HtmlPanel
-import org.lobobrowser.html.test.{SimpleHtmlRendererContext, SimpleUserAgentContext}
-
-
-class HTML_Panel extends HtmlPanel
-{
- Swing_Thread.require()
-
- Logger.getLogger("org.lobobrowser").setLevel(Level.WARNING)
-
- private val ucontext = new SimpleUserAgentContext
- private val rcontext = new SimpleHtmlRendererContext(this, ucontext)
- private val builder = new DocumentBuilderImpl(ucontext, rcontext)
-
- def render_document(url: String, html_text: String)
- {
- val doc = builder.parse(new InputSourceImpl(new StringReader(html_text), url))
- Swing_Thread.later { setDocument(doc, rcontext) }
- }
-}
--- a/src/Tools/jEdit/src/jEdit.props Sat Sep 21 16:08:17 2013 +0200
+++ b/src/Tools/jEdit/src/jEdit.props Sat Sep 21 16:44:31 2013 +0200
@@ -186,7 +186,6 @@
isabelle-output.dock-position=bottom
isabelle-output.height=174
isabelle-output.width=412
-isabelle-readme.dock-position=bottom
isabelle-sledgehammer.dock-position=bottom
isabelle-symbols.dock-position=bottom
isabelle-theories.dock-position=right
--- a/src/Tools/jEdit/src/readme_dockable.scala Sat Sep 21 16:08:17 2013 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-/* Title: Tools/jEdit/src/readme_dockable.scala
- Author: Makarius
-
-Dockable window for README.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import org.gjt.sp.jedit.View
-
-
-class README_Dockable(view: View, position: String) extends Dockable(view, position)
-{
- private val readme = new HTML_Panel
- private val readme_path = Path.explode("$JEDIT_HOME/README.html")
- readme.render_document(Isabelle_System.platform_file_url(readme_path), File.read(readme_path))
-
- set_content(readme)
-}