--- a/lib/Tools/build_dialog Fri Dec 14 19:51:20 2012 +0100
+++ b/lib/Tools/build_dialog Sat Dec 15 14:38:37 2012 +0100
@@ -12,14 +12,15 @@
function usage()
{
echo
- echo "Usage: isabelle $PRG [OPTIONS] LOGIC"
+ echo "Usage: isabelle $PRG [OPTIONS]"
echo
echo " Options are:"
echo " -L OPTION default logic via system option"
echo " -d DIR include session directory"
+ echo " -l NAME logic session name"
echo " -s system build mode: produce output in ISABELLE_HOME"
echo
- echo " Build Isabelle session image LOGIC via GUI dialog."
+ echo " Build Isabelle logic session image via GUI dialog (default: $ISABELLE_LOGIC)."
echo
exit 1
}
@@ -35,9 +36,10 @@
LOGIC_OPTION=""
declare -a INCLUDE_DIRS=()
+LOGIC=""
SYSTEM_MODE=false
-while getopts "L:d:s" OPT
+while getopts "L:d:l:s" OPT
do
case "$OPT" in
L)
@@ -46,6 +48,9 @@
d)
INCLUDE_DIRS["${#INCLUDE_DIRS[@]}"]="$OPTARG"
;;
+ l)
+ LOGIC="$OPTARG"
+ ;;
s)
SYSTEM_MODE="true"
;;
@@ -60,9 +65,7 @@
# args
-[ "$#" -ne 1 ] && usage
-
-LOGIC="$1"; shift
+[ "$#" -ne 0 ] && usage
## main
@@ -70,5 +73,5 @@
[ -e "$ISABELLE_HOME/Admin/build" ] && { "$ISABELLE_HOME/Admin/build" jars || exit $?; }
"$ISABELLE_TOOL" java isabelle.Build_Dialog \
- "$LOGIC_OPTION" "$SYSTEM_MODE" "$LOGIC" "${INCLUDE_DIRS[@]}"
+ "$LOGIC_OPTION" "$LOGIC" "$SYSTEM_MODE" "${INCLUDE_DIRS[@]}"
--- a/src/Doc/System/Sessions.thy Fri Dec 14 19:51:20 2012 +0100
+++ b/src/Doc/System/Sessions.thy Sat Dec 15 14:38:37 2012 +0100
@@ -348,16 +348,18 @@
Options are:
-L OPTION default logic via system option
-d DIR include session directory
+ -l NAME logic session name
-s system build mode: produce output in ISABELLE_HOME
- Build Isabelle session image LOGIC via GUI dialog.
+ Build Isabelle logic session image via GUI dialog (default: \$ISABELLE_LOGIC).
\end{ttbox}
- \medskip Option @{verbatim "-L"} specifies a system option name as
- fall-back, if the specified @{text "LOGIC"} name is empty.
+ \medskip Option @{verbatim "-l"} specifies an explicit logic session
+ name. Option @{verbatim "-L"} specifies a system option name as
+ fall-back to determine the logic session name. If both are omitted
+ or have empty value, @{setting ISABELLE_LOGIC} is used as default.
\medskip Options @{verbatim "-d"} and @{verbatim "-s"} have the same
- meaning as for the command-line @{tool build} tool itself.
-*}
+ meaning as for the command-line @{tool build} tool itself. *}
end
--- a/src/Pure/General/pretty.ML Fri Dec 14 19:51:20 2012 +0100
+++ b/src/Pure/General/pretty.ML Sat Dec 15 14:38:37 2012 +0100
@@ -163,9 +163,11 @@
val paragraph = markup Markup.paragraph;
val para = paragraph o text;
-fun markup_chunks m prts = markup m (fbreaks prts);
+fun markup_chunks m prts = markup m (fbreaks (map (mark Markup.text_fold) prts));
val chunks = markup_chunks Markup.empty;
-fun chunks2 prts = blk (0, flat (Library.separate [fbrk, fbrk] (map single prts)));
+
+fun chunks2 prts =
+ blk (0, flat (Library.separate [fbrk, fbrk] (map (single o mark Markup.text_fold) prts)));
fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];
--- a/src/Pure/PIDE/command.scala Fri Dec 14 19:51:20 2012 +0100
+++ b/src/Pure/PIDE/command.scala Sat Dec 15 14:38:37 2012 +0100
@@ -39,6 +39,8 @@
if (this eq other) this
else if (rep.isEmpty) other
else (this /: other.entries)(_ + _)
+
+ override def toString: String = entries.mkString("Results(", ", ", ")")
}
--- a/src/Pure/PIDE/markup.ML Fri Dec 14 19:51:20 2012 +0100
+++ b/src/Pure/PIDE/markup.ML Sat Dec 15 14:38:37 2012 +0100
@@ -77,6 +77,7 @@
val document_antiquotationN: string
val document_antiquotation_optionN: string
val paragraphN: string val paragraph: T
+ val text_foldN: string val text_fold: T
val keywordN: string val keyword: T
val operatorN: string val operator: T
val commandN: string val command: T
@@ -95,7 +96,8 @@
val subgoalsN: string
val proof_stateN: string val proof_state: int -> T
val stateN: string val state: T
- val subgoalN: string val subgoal: T
+ val goalN: string val goal: T
+ val subgoalN: string val subgoal: string -> T
val taskN: string
val acceptedN: string val accepted: T
val forkedN: string val forked: T
@@ -297,6 +299,7 @@
(* text structure *)
val (paragraphN, paragraph) = markup_elem "paragraph";
+val (text_foldN, text_fold) = markup_elem "text_fold";
(* outer syntax *)
@@ -337,7 +340,8 @@
val (proof_stateN, proof_state) = markup_int "proof_state" subgoalsN;
val (stateN, state) = markup_elem "state";
-val (subgoalN, subgoal) = markup_elem "subgoal";
+val (goalN, goal) = markup_elem "goal";
+val (subgoalN, subgoal) = markup_string "subgoal" nameN;
(* command status *)
--- a/src/Pure/PIDE/markup.scala Fri Dec 14 19:51:20 2012 +0100
+++ b/src/Pure/PIDE/markup.scala Sat Dec 15 14:38:37 2012 +0100
@@ -145,6 +145,7 @@
/* text structure */
val PARAGRAPH = "paragraph"
+ val TEXT_FOLD = "text_fold"
/* ML syntax */
@@ -210,6 +211,7 @@
val PROOF_STATE = "proof_state"
val STATE = "state"
+ val GOAL = "goal"
val SUBGOAL = "subgoal"
--- a/src/Pure/System/build_dialog.scala Fri Dec 14 19:51:20 2012 +0100
+++ b/src/Pure/System/build_dialog.scala Sat Dec 15 14:38:37 2012 +0100
@@ -18,12 +18,13 @@
{
def main(args: Array[String]) =
{
+ Platform.init_laf()
try {
args.toList match {
case
logic_option ::
+ logic ::
Properties.Value.Boolean(system_mode) ::
- logic ::
include_dirs =>
val more_dirs = include_dirs.map(s => ((false, Path.explode(s))))
@@ -36,8 +37,6 @@
more_dirs = more_dirs, sessions = List(session)) == 0) sys.exit(0)
else
Swing_Thread.later {
- Platform.init_laf()
-
val top = build_dialog(options, system_mode, more_dirs, session)
top.pack()
--- a/src/Pure/goal_display.ML Fri Dec 14 19:51:20 2012 +0100
+++ b/src/Pure/goal_display.ML Sat Dec 15 14:38:37 2012 +0100
@@ -115,9 +115,9 @@
fun pretty_list _ _ [] = []
| pretty_list name prt lst = [Pretty.big_list name (map prt lst)];
- fun pretty_subgoal (n, A) =
- Pretty.markup Markup.subgoal [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A];
- fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As);
+ fun pretty_subgoal s A =
+ Pretty.markup (Markup.subgoal s) [Pretty.str (" " ^ s ^ ". "), prt_term A];
+ val pretty_subgoals = map_index (fn (i, A) => pretty_subgoal (string_of_int (i + 1)) A);
val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt);
@@ -130,7 +130,7 @@
val (As, B) = Logic.strip_horn prop;
val ngoals = length As;
in
- (if show_main_goal then [prt_term B] else []) @
+ (if show_main_goal then [Pretty.mark Markup.goal (prt_term B)] else []) @
(if ngoals = 0 then [Pretty.str "No subgoals!"]
else if ngoals > goals_limit then
pretty_subgoals (take goals_limit As) @
--- a/src/Pure/library.scala Fri Dec 14 19:51:20 2012 +0100
+++ b/src/Pure/library.scala Sat Dec 15 14:38:37 2012 +0100
@@ -128,7 +128,7 @@
/* simple dialogs */
- def scrollable_text(txt: String, width: Int = 80, editable: Boolean = false): ScrollPane =
+ def scrollable_text(txt: String, width: Int = 60, editable: Boolean = false): ScrollPane =
{
val text = new TextArea(txt)
if (width > 0) text.columns = width
--- a/src/Tools/jEdit/README.html Fri Dec 14 19:51:20 2012 +0100
+++ b/src/Tools/jEdit/README.html Sat Dec 15 14:38:37 2012 +0100
@@ -157,17 +157,17 @@
</ul>
-<h2>Limitations and workarounds</h2>
+<h2>Limitations and known problems</h2>
<ul>
- <li>Odd behavior of some diagnostic commands, notably those starting
- external processes asynchronously (e.g. <tt>thy_deps</tt>).<br/>
- <em>Workaround:</em> Avoid such commands.</li>
-
<li>Lack of dependency managed 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
@@ -176,21 +176,14 @@
<li>No support for non-local markup, e.g. commands reporting on
previous commands (proof end on proof head), or markup produced by
loading external files.</li>
-</ul>
-
-
-<h2>Known problems with Mac OS X</h2>
-
-<ul>
-<li>The MacOSX plugin for jEdit disrupts tends to be disruptive. It
-might or might not improve the user experience, and is off by
-default.</li>
+ <li>The native MacOSX plugin for jEdit tends to be disruptive. It
+ might or might not improve the user experience, and is off by
+ default.</li>
-<li>Java 7 (by Oracle) is officially supported starting with Lion (or
-later), but not Snow Leopard. It happens to work on the latter as
-well, but there might be some instabilities.</li>
-
+ <li>Java 7 on MacOSX is officially supported on Lion and Mountain
+ Lion, but not Snow Leopard. It usually works on the latter, but
+ there might be some instabilities.</li>
</ul>
--- a/src/Tools/jEdit/lib/Tools/jedit Fri Dec 14 19:51:20 2012 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit Sat Dec 15 14:38:37 2012 +0100
@@ -12,6 +12,7 @@
"src/dockable.scala"
"src/document_model.scala"
"src/document_view.scala"
+ "src/fold_handling.scala"
"src/graphview_dockable.scala"
"src/html_panel.scala"
"src/hyperlink.scala"
@@ -96,7 +97,7 @@
# options
-declare -a BUILD_DIALOG_OPTIONS=()
+declare -a BUILD_DIALOG_OPTIONS=(-L jedit_logic)
BUILD_ONLY=false
BUILD_JARS="jars"
@@ -133,6 +134,8 @@
ARGS["${#ARGS[@]}"]="$OPTARG"
;;
l)
+ BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="-l"
+ BUILD_DIALOG_OPTIONS["${#BUILD_DIALOG_OPTIONS[@]}"]="$OPTARG"
JEDIT_LOGIC="$OPTARG"
;;
m)
@@ -327,7 +330,7 @@
if [ "$BUILD_ONLY" = false ]; then
if [ "$NO_BUILD" = false ]; then
- "$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}" -L jedit_logic "$JEDIT_LOGIC"
+ "$ISABELLE_TOOL" build_dialog "${BUILD_DIALOG_OPTIONS[@]}"
RC="$?"
[ "$RC" = 0 ] || exit "$RC"
fi
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/fold_handling.scala Sat Dec 15 14:38:37 2012 +0100
@@ -0,0 +1,48 @@
+/* Title: Tools/jEdit/src/fold_handler.scala
+ Author: Makarius
+
+Handling of folds within the text structure.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import org.gjt.sp.jedit.buffer.{JEditBuffer, FoldHandler}
+
+import javax.swing.text.Segment
+
+
+object Fold_Handling
+{
+ class Document_Fold_Handler(private val rendering: Rendering)
+ extends FoldHandler("isabelle-document")
+ {
+ override def equals(other: Any): Boolean =
+ other match {
+ case that: Document_Fold_Handler => this.rendering == that.rendering
+ case _ => false
+ }
+
+ override def getFoldLevel(buffer: JEditBuffer, line: Int, seg: Segment): Int =
+ {
+ def depth(i: Text.Offset): Int =
+ if (i < 0) 0
+ else {
+ rendering.fold_depth(Text.Range(i, i + 1)).map(_.info) match {
+ case d #:: _ => d
+ case _ => 0
+ }
+ }
+
+ if (line <= 0) 0
+ else {
+ val start = buffer.getLineStartOffset(line - 1)
+ val end = buffer.getLineEndOffset(line - 1)
+ buffer.getFoldLevel(line - 1) - depth(start - 1) + depth(end - 1)
+ }
+ }
+ }
+}
+
--- a/src/Tools/jEdit/src/output_dockable.scala Fri Dec 14 19:51:20 2012 +0100
+++ b/src/Tools/jEdit/src/output_dockable.scala Sat Dec 15 14:38:37 2012 +0100
@@ -37,7 +37,7 @@
/* pretty text area */
- private val pretty_text_area = new Pretty_Text_Area(view)
+ val pretty_text_area = new Pretty_Text_Area(view)
set_content(pretty_text_area)
--- a/src/Tools/jEdit/src/pretty_text_area.scala Fri Dec 14 19:51:20 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala Sat Dec 15 14:38:37 2012 +0100
@@ -10,12 +10,13 @@
import isabelle._
-import java.awt.{Font, FontMetrics, Toolkit}
+import java.awt.{Color, Font, FontMetrics, Toolkit}
import java.awt.event.{ActionListener, ActionEvent, KeyEvent}
import javax.swing.{KeyStroke, JComponent}
import org.gjt.sp.jedit.{jEdit, View, Registers}
import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea}
+import org.gjt.sp.jedit.syntax.SyntaxStyle
import org.gjt.sp.util.SyntaxUtilities
@@ -52,7 +53,9 @@
}
}
-class Pretty_Text_Area(view: View) extends JEditEmbeddedTextArea
+class Pretty_Text_Area(
+ view: View,
+ background: Option[Color] = None) extends JEditEmbeddedTextArea
{
text_area =>
@@ -80,9 +83,33 @@
getPainter.setAntiAlias(new AntiAlias(jEdit.getProperty("view.antiAlias")))
getPainter.setStyles(SyntaxUtilities.loadStyles(current_font_family, current_font_size))
+ val fold_line_style = new Array[SyntaxStyle](4)
+ for (i <- 0 to 3) {
+ fold_line_style(i) =
+ SyntaxUtilities.parseStyle(
+ jEdit.getProperty("view.style.foldLine." + i),
+ current_font_family, current_font_size, true)
+ }
+ getPainter.setFoldLineStyle(fold_line_style)
+
if (getWidth > 0) {
+ getGutter.setForeground(jEdit.getColorProperty("view.gutter.fgColor"))
+ getGutter.setBackground(jEdit.getColorProperty("view.gutter.bgColor"))
+ background.map(bg => { getPainter.setBackground(bg); getGutter.setBackground(bg) })
+ getGutter.setHighlightedForeground(jEdit.getColorProperty("view.gutter.highlightColor"))
+ getGutter.setFoldColor(jEdit.getColorProperty("view.gutter.foldColor"))
+ getGutter.setFont(jEdit.getFontProperty("view.gutter.font"))
+ getGutter.setBorder(0,
+ jEdit.getColorProperty("view.gutter.focusBorderColor"),
+ jEdit.getColorProperty("view.gutter.noFocusBorderColor"),
+ getPainter.getBackground)
+ getGutter.setFoldPainter(getFoldPainter)
+
+ getGutter.setGutterEnabled(jEdit.getBooleanProperty("view.gutter.enabled"))
+
val font_metrics = getPainter.getFontMetrics(font)
- val margin = (getWidth / (font_metrics.charWidth(Pretty.spc) max 1) - 2) max 20
+ val margin =
+ ((getWidth - getGutter.getWidth) / (font_metrics.charWidth(Pretty.spc) max 1) - 2) max 20
val base_snapshot = current_base_snapshot
val base_results = current_base_results
@@ -100,6 +127,7 @@
JEdit_Lib.buffer_edit(getBuffer) {
rich_text_area.active_reset()
getBuffer.setReadOnly(false)
+ getBuffer.setFoldHandler(new Fold_Handling.Document_Fold_Handler(rendering))
setText(text)
setCaretPosition(0)
getBuffer.setReadOnly(true)
--- a/src/Tools/jEdit/src/pretty_tooltip.scala Fri Dec 14 19:51:20 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_tooltip.scala Sat Dec 15 14:38:37 2012 +0100
@@ -68,8 +68,7 @@
/* pretty text area */
- val pretty_text_area = new Pretty_Text_Area(view)
- pretty_text_area.getPainter.setBackground(rendering.tooltip_color)
+ val pretty_text_area = new Pretty_Text_Area(view, Some(rendering.tooltip_color))
pretty_text_area.resize(Rendering.font_family(),
Rendering.font_size("jedit_tooltip_font_scale").round)
pretty_text_area.update(rendering.snapshot, results, body)
--- a/src/Tools/jEdit/src/rendering.scala Fri Dec 14 19:51:20 2012 +0100
+++ b/src/Tools/jEdit/src/rendering.scala Sat Dec 15 14:38:37 2012 +0100
@@ -158,16 +158,18 @@
val overview_limit = options.int("jedit_text_overview_limit")
+ private val overview_include = Protocol.command_status_markup + Markup.WARNING + Markup.ERROR
+
def overview_color(range: Text.Range): Option[Color] =
{
if (snapshot.is_outdated) None
else {
val results =
snapshot.cumulate_markup[(Protocol.Status, Int)](
- range, (Protocol.Status.init, 0),
- Some(Protocol.command_status_markup + Markup.WARNING + Markup.ERROR), _ =>
+ range, (Protocol.Status.init, 0), Some(overview_include), _ =>
{
- case ((status, pri), Text.Info(_, XML.Elem(markup, _))) =>
+ case ((status, pri), Text.Info(_, XML.Elem(markup, _)))
+ if overview_include(markup.name) =>
if (markup.name == Markup.WARNING || markup.name == Markup.ERROR)
(status, pri max Rendering.message_pri(markup.name))
else (Protocol.command_status(status, markup), pri)
@@ -527,4 +529,16 @@
if text_colors.isDefinedAt(m) => text_colors(m)
})
}
+
+
+ /* nested text structure -- folds */
+
+ private val fold_depth_include = Set(Markup.TEXT_FOLD, Markup.GOAL, Markup.SUBGOAL)
+
+ def fold_depth(range: Text.Range): Stream[Text.Info[Int]] =
+ snapshot.cumulate_markup[Int](range, 0, Some(fold_depth_include), _ =>
+ {
+ case (depth, Text.Info(_, XML.Elem(Markup(name, _), _)))
+ if fold_depth_include(name) => depth + 1
+ })
}