Welcome to the Isabelle/jEdit Prover IDE

# HG changeset patch # User wenzelm # Date 1379774671 -7200 # Node ID 30de372ca56ffa2d24c3b09f70800c8028aec22f # Parent 17e93676670b7f091df81326866832e35d79fa0e removed obsolete README; open Documentation dockable by default; diff -r 17e93676670b -r 30de372ca56f src/Pure/Tools/main.scala --- 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"), - """""") + """""") File.write(settings_dir + Path.explode("perspective.xml"), """ diff -r 17e93676670b -r 30de372ca56f src/Tools/jEdit/README.html --- 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 @@ - - - - - - - -Welcome to the Isabelle/jEdit Prover IDE - - - - -

- -

- PIDE is a framework for Prover IDEs based on the - Isabelle/Scala. It is built around a concept of - asynchronous document processing, which is supported - natively by the parallel proof engine that is implemented - in Isabelle/ML. -

- -

- Isabelle/jEdit is the main example application of the PIDE - framework — it is ready for small and large Isabelle - applications, for beginners and experts alike. -

- -

- 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). -

- - - -

The Isabelle/jEdit Prover IDE

- -

-Isabelle/jEdit consists of some plugins for the well-known jEdit text -editor framework (http://www.jedit.org), according to the following -principles. -

- -

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).
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.
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.
Using the mouse together with the modifier key CONTROL (Linux, -Windows) or COMMAND (Mac OS X) exposes additional formal -content.
Dockable panels (e.g. Output, Symbols) are managed as -independent windows by jEdit, which also allows multiple instances.
Formal output (in popups etc.) may be explored recursively, using the -same techniques as in the editor source buffer.
The prover process and source files are managed on the editor side. The -prover operates on timeless and stateless document content via -Isabelle/Scala.
Plugin options of jEdit (for the Isabelle 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.
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.

- - -

Isabelle symbols and fonts

- -

Isabelle supports infinitely many symbols:
- α, β, γ, …
- ∀, ∃, ∨, ∧, ⟶, ⟷, …
- ≤, ≥, ⊓, ⊔, …
- ℵ, △, ∇, …
- \<foo>, \<bar>, \<baz>, …
-
There are some special control symbols to modify the style of a - single symbol:
- ⇩ subscript
- ⇧ superscript
- ⇣ subscript within identifier
- ⇡ superscript within identifier
- ❙ bold face
A default mapping relates some Isabelle symbols to Unicode points - (see $ISABELLE_HOME/etc/symbols and $ISABELLE_HOME_USER/etc/symbols). -
The IsabelleText font ensures that Unicode points are actually - seen on the screen (or printer). -

Input methods: -

use the Symbols dockable
copy/paste from decoded source files
copy/paste from prover output

completion provided by Isabelle plugin, e.g.
- - - - - - - - - - - - - - - - - - - - - - - - - -

name	abbreviation	symbol
lambda	`%`	λ
Rightarrow	`=>`	⇒
Longrightarrow	`==>`	⟹
And	`!!`	⋀
equiv	`==`	≡
forall	`!`	∀
exists	`?`	∃
longrightarrow	`-->`	⟶
and	`/\`	∧
or	`\/`	∨
not	`~`	¬
noteq	`~=`	≠
in	`:`	∈
notin	`~:`	∉
sub	`=_`	⇩
sup	`=^`	⇧
bold	`-.`	❙

NOTE: The above abbreviations refer to the input method. - The logical notation provides ASCII alternatives that often - coincide, but deviate occasionally. -
NOTE: 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. -
NOTE: 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. -
NOTE: Control symbols may be applied to a region of selected - text, either using the Symbols dockable or keyboard shortcuts.

- - -

Limitations and known problems

- -

Keyboard shortcuts C-PLUS and C-MINUS for adjusting the editor font - size depend on platform details and national keyboards.
- Workaround: Use numeric keypad or rebind keys in the jEdit Shortcuts - options dialog.
Lack of dependency management for auxiliary files that contribute - to a theory (e.g. ML_file).
- Workaround: Re-load files manually within the prover.
Odd behavior of some diagnostic commands with global - side-effects, like writing a physical - file.
- Workaround: Avoid such commands.
No way to delete document nodes from the overall collection of - theories.
- Workaround: Restart whole Isabelle/jEdit session in - worst-case situation.
Linux: some desktop environments with extreme animation effects - may disrupt Java 7 window placement and keyboard focus.
- Workaround: Disable such effects.
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 - awesome or xmonad.
- Workaround: Use regular re-parenting window manager.
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.
- Workaround: Disable MacOSX plugin.
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.
- Workaround: Update to OS X Mountain Lion.

- - -

Licenses and home sites of contributing systems

- -

Isabelle: BSD-style
Poly/ML: LGPL
http://www.polyml.org
Scala: BSD-style
http://www.scala-lang.org
jEdit: GPL (with special cases)
http://www.jedit.org
JFreeChart: LGPL
http://www.jfree.org
Lobo/Cobra: GPL and LGPL
http://lobobrowser.org

- - - diff -r 17e93676670b -r 30de372ca56f src/Tools/jEdit/lib/Tools/jedit --- 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" diff -r 17e93676670b -r 30de372ca56f src/Tools/jEdit/src/Isabelle.props --- 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 diff -r 17e93676670b -r 30de372ca56f src/Tools/jEdit/src/actions.xml --- 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"); - -


-			wm.addDockableWindow("isabelle-readme");
-


 			wm.addDockableWindow("isabelle-find");
diff -r 17e93676670b -r 30de372ca56f src/Tools/jEdit/src/dockables.xml
--- 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 @@
 	
 		new isabelle.jedit.Documentation_Dockable(view, position);
 	
-	
-		new isabelle.jedit.README_Dockable(view, position);
-	
 	
 		new isabelle.jedit.Output_Dockable(view, position);
 	
diff -r 17e93676670b -r 30de372ca56f src/Tools/jEdit/src/html_panel.scala
--- 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) }
-  }
-}
diff -r 17e93676670b -r 30de372ca56f src/Tools/jEdit/src/jEdit.props
--- 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
diff -r 17e93676670b -r 30de372ca56f src/Tools/jEdit/src/readme_dockable.scala
--- 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)
-}