src/Doc/JEdit/JEdit.thy
 changeset 54320 b8bd31c7058c parent 54037 ab77ec347220 child 54321 41951f427ac7
equal inserted replaced
54319:219dd1028399 54320:b8bd31c7058c
    23 \item [PIDE] is a general framework for Prover IDEs based on the
    23 \item [PIDE] is a general framework for Prover IDEs based on the
    24 Isabelle/Scala. It is built around a concept of \emph{asynchronous document
    24 Isabelle/Scala. It is built around a concept of \emph{asynchronous document
    25 processing}, which is supported natively by the \emph{parallel proof engine}
    25 processing}, which is supported natively by the \emph{parallel proof engine}
    26 that is implemented in Isabelle/ML.
    26 that is implemented in Isabelle/ML.
    27
    27
    28 \item [jEdit] is a sophisticated text editor \url{http://www.jedit.org}
    28 \item [jEdit] is a sophisticated text
    29 implemented in Java. It is easily extensible by plugins written in any
    29 editor\footnote{\url{http://www.jedit.org}} implemented in Java. It is easily
    30 language that works on the JVM, e.g.\ Scala.
    30 extensible by plugins written in languages that work on the JVM, e.g.\

    31 Scala\footnote{\url{http://www.scala-lang.org/}}.
    31
    32
    32 \item [Isabelle/jEdit] is the main example application of the PIDE framework
    33 \item [Isabelle/jEdit] is the main example application of the PIDE framework
    33 and the default user-interface for Isabelle. It is targeted at beginners and
    34 and the default user-interface for Isabelle. It is targeted at beginners and
    34 experts alike.
    35 experts alike.
    35
    36
    78   to a selection of Isabelle/Scala options and its persistence preferences,
    79   to a selection of Isabelle/Scala options and its persistence preferences,
    79   usually with immediate effect on the prover back-end or editor front-end.
    80   usually with immediate effect on the prover back-end or editor front-end.
    80
    81
    81   \item The logic image of the prover session may be specified within
    82   \item The logic image of the prover session may be specified within
    82   Isabelle/jEdit, but this requires restart. The new image is provided
    83   Isabelle/jEdit, but this requires restart. The new image is provided
    83   automatically by the Isabelle build process.
    84   automatically by the Isabelle build tool.
    84
    85
    85   \end{itemize}
    86   \end{itemize}
    86 *}
    87 *}
    87
    88
    88
    89
   187   of the time and continue typing quickly.
   188   of the time and continue typing quickly.
   188
   189
   189   Various Isabelle plugin options control the popup behavior and immediate
   190   Various Isabelle plugin options control the popup behavior and immediate
   190   insertion into buffer.
   191   insertion into buffer.
   191
   192
   192   Isabelle Symbols are completed in backslashed forms, e.g. @{verbatim
   193   Isabelle Symbols are completed in backslashed forms, e.g.\ @{verbatim
   193   "\\"}@{verbatim "forall"} or @{verbatim "\<forall>"} that both produce the Isabelle
   194   "\\"}@{verbatim "forall"} or @{verbatim "\<forall>"} that both produce the Isabelle
   194   symbol @{text "\<forall>"} in its Unicode rendering. Alternatively, symbol
   195   symbol @{text "\<forall>"} in its Unicode rendering. Alternatively, symbol
   195   abbreviations may be used as specified in @{file
   196   abbreviations may be used as specified in @{file
   196   "$ISABELLE_HOME/etc/symbols"}.  197 "$ISABELLE_HOME/etc/symbols"}.
   197
   198