src/Tools/jEdit/README
author wenzelm
Thu Sep 02 00:48:07 2010 +0200 (2010-09-02)
changeset 38980 af73cf0dc31f
parent 37862 ec81023c6861
child 39245 cc155a9bf3a2
permissions -rw-r--r--
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
tuned;
     1 Isabelle/jEdit based on Isabelle/Scala
     2 ======================================
     3 
     4 The Isabelle/Scala layer that is already part of Isabelle/Pure
     5 provides some general infrastructure for advanced prover interaction
     6 and integration.  The Isabelle/jEdit application serves as an example
     7 for asynchronous proof checking with support for parallel processing.
     8 
     9 See also the paper:
    10 
    11   Makarius Wenzel. Asynchronous Proof Processing with Isabelle/Scala
    12   and Isabelle/jEdit. In C. Sacerdoti Coen and D. Aspinall, editors,
    13   User Interfaces for Theorem Provers (UITP 2010), FLOC 2010 Satellite
    14   Workshop, Edinburgh, Scotland, July 2010. To appear in ENTCS.
    15   http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf
    16 
    17 
    18 Some limitations of the current implementation (as of Isabelle2009-2):
    19 
    20   * No provisions for editing multiple theory files.
    21 
    22   * No reclaiming of old/unused document versions.  Memory will fill
    23     up eventually, both on the JVM and ML side.
    24 
    25   * No support for non-local markup, e.g. commands reporting on
    26     previous commands (proof end on proof head), or markup produced by
    27     loading external files.
    28 
    29   * Some performance bottlenecks for massive amount of markup,
    30     e.g. when processing large ML sections.
    31 
    32   * General lack of various conveniences known from Proof General.
    33 
    34 Despite these shortcomings, Isabelle/jEdit already demonstrates that
    35 interactive theorem proving can be much more than command-line
    36 interaction via TTY or editor front-ends (such as Proof General and
    37 its many remakes).
    38 
    39 
    40 Known problems with Mac OS
    41 ==========================
    42 
    43 - The MacOSX plugin for jEdit disrupts regular C-X/C/V operations,
    44   e.g. between the editor and the Console plugin, which is a standard
    45   swing text box.  Similar for search boxes etc.
    46 
    47 - ToggleButton selected state is not rendered if window focus is lost,
    48   which is probably a genuine feature of the Apple look-and-feel.
    49 
    50 - Anti-aliasing does not really work as well as for Linux or Windows.
    51   (General Apple/Swing problem?)
    52 
    53 - Font.createFont mangles the font family of non-regular fonts,
    54   e.g. bold.  IsabelleText font files need to be installed manually.
    55 
    56 - Missing glyphs are collected from other fonts (like Emacs, Firefox).
    57   This is actually an advantage over the Oracle/Sun JVM on Windows or
    58   Linux, but probably also the deeper reason for the other oddities of
    59   Apple font management.
    60 
    61 
    62 Windows/Linux
    63 =============
    64 
    65 - Works best with Sun Java 1.6.x -- avoid OpenJDK for now.
    66 
    67 
    68 Licenses and home sites of contributing systems
    69 ===============================================
    70 
    71 * Scala: BSD-style
    72   http://www.scala-lang.org
    73 
    74 * jEdit: GPL (with special cases)
    75   http://www.jedit.org/
    76 
    77 * Lobo/Cobra: GPL and LGPL
    78   http://lobobrowser.org/
    79 
    80 
    81      Makarius
    82      31-May-2010