# HG changeset patch # User wenzelm # Date 1355578717 -3600 # Node ID 91c716c848c25276a0335472eea6d39767867d8e # Parent 0aec55e637958c8c71592bef915bc1bc00bd016e# Parent ebd75dfaab73999ea98ff8de0f309199775c0c66 merged diff -r 0aec55e63795 -r 91c716c848c2 lib/Tools/build_dialog --- 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[@]}" diff -r 0aec55e63795 -r 91c716c848c2 src/Doc/System/Sessions.thy --- 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 diff -r 0aec55e63795 -r 91c716c848c2 src/Pure/General/pretty.ML --- 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]; diff -r 0aec55e63795 -r 91c716c848c2 src/Pure/PIDE/command.scala --- 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(", ", ", ")") } diff -r 0aec55e63795 -r 91c716c848c2 src/Pure/PIDE/markup.ML --- 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 *) diff -r 0aec55e63795 -r 91c716c848c2 src/Pure/PIDE/markup.scala --- 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" diff -r 0aec55e63795 -r 91c716c848c2 src/Pure/System/build_dialog.scala --- 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() diff -r 0aec55e63795 -r 91c716c848c2 src/Pure/goal_display.ML --- 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) @ diff -r 0aec55e63795 -r 91c716c848c2 src/Pure/library.scala --- 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 diff -r 0aec55e63795 -r 91c716c848c2 src/Tools/jEdit/README.html --- 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 @@ -

Limitations and workarounds

+

Limitations and known problems

- - -

Known problems with Mac OS X

- - diff -r 0aec55e63795 -r 91c716c848c2 src/Tools/jEdit/lib/Tools/jedit --- 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 diff -r 0aec55e63795 -r 91c716c848c2 src/Tools/jEdit/src/fold_handling.scala --- /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) + } + } + } +} + diff -r 0aec55e63795 -r 91c716c848c2 src/Tools/jEdit/src/output_dockable.scala --- 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) diff -r 0aec55e63795 -r 91c716c848c2 src/Tools/jEdit/src/pretty_text_area.scala --- 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) diff -r 0aec55e63795 -r 91c716c848c2 src/Tools/jEdit/src/pretty_tooltip.scala --- 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) diff -r 0aec55e63795 -r 91c716c848c2 src/Tools/jEdit/src/rendering.scala --- 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 + }) }