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