--- a/src/Pure/General/markup.ML Wed Sep 08 13:30:41 2010 +0100
+++ b/src/Pure/General/markup.ML Wed Sep 08 14:46:21 2010 +0200
@@ -58,6 +58,7 @@
val literalN: string val literal: T
val inner_stringN: string val inner_string: T
val inner_commentN: string val inner_comment: T
+ val token_rangeN: string val token_range: T
val sortN: string val sort: T
val typN: string val typ: T
val termN: string val term: T
@@ -119,6 +120,7 @@
val promptN: string val prompt: T
val readyN: string val ready: T
val reportN: string val report: T
+ val badN: string val bad: T
val no_output: output * output
val default_output: T -> output * output
val add_mode: string -> (T -> output * output) -> unit
@@ -239,6 +241,8 @@
val (inner_stringN, inner_string) = markup_elem "inner_string";
val (inner_commentN, inner_comment) = markup_elem "inner_comment";
+val (token_rangeN, token_range) = markup_elem "token_range";
+
val (sortN, sort) = markup_elem "sort";
val (typN, typ) = markup_elem "typ";
val (termN, term) = markup_elem "term";
@@ -345,6 +349,8 @@
val (reportN, report) = markup_elem "report";
+val (badN, bad) = markup_elem "bad";
+
(** print mode operations **)
--- a/src/Pure/General/markup.scala Wed Sep 08 13:30:41 2010 +0100
+++ b/src/Pure/General/markup.scala Wed Sep 08 14:46:21 2010 +0200
@@ -136,6 +136,8 @@
val LITERAL = "literal"
val INNER_COMMENT = "inner_comment"
+ val TOKEN_RANGE = "token_range"
+
val SORT = "sort"
val TYP = "typ"
val TERM = "term"
@@ -247,6 +249,8 @@
val SIGNAL = "signal"
val EXIT = "exit"
+ val BAD = "bad"
+
val Ready = Markup("ready", Nil)
--- a/src/Pure/Isar/proof_context.ML Wed Sep 08 13:30:41 2010 +0100
+++ b/src/Pure/Isar/proof_context.ML Wed Sep 08 14:46:21 2010 +0200
@@ -736,18 +736,22 @@
local
+fun parse_failed ctxt pos msg kind =
+ (Context_Position.report ctxt Markup.bad pos;
+ cat_error msg ("Failed to parse " ^ kind));
+
fun parse_sort ctxt text =
let
val (syms, pos) = Syntax.parse_token ctxt Markup.sort text;
val S = Syntax.standard_parse_sort ctxt (syn_of ctxt) (syms, pos)
- handle ERROR msg => cat_error msg "Failed to parse sort";
+ handle ERROR msg => parse_failed ctxt pos msg "sort";
in Type.minimize_sort (tsig_of ctxt) S end;
fun parse_typ ctxt text =
let
val (syms, pos) = Syntax.parse_token ctxt Markup.typ text;
val T = Syntax.standard_parse_typ ctxt (syn_of ctxt) (get_sort ctxt) (syms, pos)
- handle ERROR msg => cat_error msg "Failed to parse type";
+ handle ERROR msg => parse_failed ctxt pos msg "type";
in T end;
fun parse_term T ctxt text =
@@ -764,7 +768,7 @@
val t =
Syntax.standard_parse_term check get_sort map_const map_free
ctxt (Type.is_logtype (tsig_of ctxt)) (syn_of ctxt) T' (syms, pos)
- handle ERROR msg => cat_error msg ("Failed to parse " ^ kind);
+ handle ERROR msg => parse_failed ctxt pos msg kind;
in t end;
--- a/src/Pure/PIDE/command.scala Wed Sep 08 13:30:41 2010 +0100
+++ b/src/Pure/PIDE/command.scala Wed Sep 08 14:46:21 2010 +0200
@@ -48,11 +48,11 @@
case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
(this /: msgs)((state, msg) =>
msg match {
- case XML.Elem(Markup(name, atts @ Position.Id_Range(id, range)), args)
- if id == command.id =>
+ case XML.Elem(Markup(name, atts @ Position.Id_Range(id, raw_range)), args)
+ if id == command.id && command.range.contains(command.decode(raw_range)) =>
+ val range = command.decode(raw_range)
val props = Position.purge(atts)
- val info =
- Text.Info[Any](command.decode(range), XML.Elem(Markup(name, props), args))
+ val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
state.add_markup(info)
case _ => System.err.println("Ignored report message: " + msg); state
})
@@ -60,8 +60,8 @@
atts match {
case Markup.Serial(i) =>
val result = XML.Elem(Markup(name, Position.purge(atts)), body)
- (add_result(i, result) /: Isar_Document.reported_positions(command.id, message))(
- (st, range) => st.add_markup(Text.Info(command.decode(range), result)))
+ (add_result(i, result) /: Isar_Document.reported_positions(command, message))(
+ (st, range) => st.add_markup(Text.Info(range, result)))
case _ => System.err.println("Ignored message without serial number: " + message); this
}
}
--- a/src/Pure/PIDE/document.scala Wed Sep 08 13:30:41 2010 +0100
+++ b/src/Pure/PIDE/document.scala Wed Sep 08 14:46:21 2010 +0200
@@ -169,11 +169,11 @@
def lookup_command(id: Command_ID): Option[Command]
def state(command: Command): Command.State
def convert(i: Text.Offset): Text.Offset
- def convert(range: Text.Range): Text.Range = range.map(convert(_))
+ def convert(range: Text.Range): Text.Range
def revert(i: Text.Offset): Text.Offset
- def revert(range: Text.Range): Text.Range = range.map(revert(_))
- def select_markup[A](range: Text.Range)
- (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]]
+ def revert(range: Text.Range): Text.Range
+ def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
+ : Stream[Text.Info[Option[A]]]
}
object State
@@ -304,18 +304,24 @@
def convert(offset: Text.Offset) = (offset /: edits)((i, edit) => edit.convert(i))
def revert(offset: Text.Offset) = (offset /: reverse_edits)((i, edit) => edit.revert(i))
- def select_markup[A](range: Text.Range)
- (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] =
+ def convert(range: Text.Range): Text.Range =
+ if (edits.isEmpty) range else range.map(convert(_))
+
+ def revert(range: Text.Range): Text.Range =
+ if (edits.isEmpty) range else range.map(revert(_))
+
+ def select_markup[A](range: Text.Range)(result: Markup_Tree.Select[A])
+ : Stream[Text.Info[Option[A]]] =
{
val former_range = revert(range)
for {
- (command, command_start) <- node.command_range(former_range)
+ (command, command_start) <- node.command_range(former_range).toStream
Text.Info(r0, x) <- state(command).markup.
select((former_range - command_start).restrict(command.range)) {
case Text.Info(r0, info)
if result.isDefinedAt(Text.Info(convert(r0 + command_start), info)) =>
result(Text.Info(convert(r0 + command_start), info))
- } { default }
+ }
val r = convert(r0 + command_start)
if !r.is_singularity
} yield Text.Info(r, x)
--- a/src/Pure/PIDE/isar_document.scala Wed Sep 08 13:30:41 2010 +0100
+++ b/src/Pure/PIDE/isar_document.scala Wed Sep 08 14:46:21 2010 +0200
@@ -61,19 +61,27 @@
private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
private val exclude_pos = Set(Markup.LOCATION)
- def reported_positions(command_id: Document.Command_ID, message: XML.Elem): Set[Text.Range] =
+ private def is_state(msg: XML.Tree): Boolean =
+ msg match {
+ case XML.Elem(Markup(Markup.WRITELN, _), List(XML.Elem(Markup(Markup.STATE, _), _))) => true
+ case _ => false
+ }
+
+ def reported_positions(command: Command, message: XML.Elem): Set[Text.Range] =
{
def reported(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
tree match {
- case XML.Elem(Markup(name, Position.Id_Range(id, range)), body)
- if include_pos(name) && id == command_id =>
- body.foldLeft(set + range)(reported)
+ case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
+ if include_pos(name) && id == command.id =>
+ val range = command.decode(raw_range).restrict(command.range)
+ body.foldLeft(if (range.is_singularity) set else set + range)(reported)
case XML.Elem(Markup(name, _), body) if !exclude_pos(name) =>
body.foldLeft(set)(reported)
case _ => set
}
val set = reported(Set.empty, message)
- if (set.isEmpty) set ++ Position.Range.unapply(message.markup.properties)
+ if (set.isEmpty && !is_state(message))
+ set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))
else set
}
}
--- a/src/Pure/PIDE/markup_tree.scala Wed Sep 08 13:30:41 2010 +0100
+++ b/src/Pure/PIDE/markup_tree.scala Wed Sep 08 14:46:21 2010 +0200
@@ -43,6 +43,8 @@
}
val empty = new Markup_Tree(Branches.empty)
+
+ type Select[A] = PartialFunction[Text.Info[Any], A]
}
@@ -89,11 +91,13 @@
private def overlapping(range: Text.Range): Stream[(Text.Range, Branches.Entry)] =
Branches.overlapping(range, branches).toStream
- def select[A](root_range: Text.Range)
- (result: PartialFunction[Text.Info[Any], A])(default: A): Iterator[Text.Info[A]] =
+ def select[A](root_range: Text.Range)(result: Markup_Tree.Select[A])
+ : Stream[Text.Info[Option[A]]] =
{
- def stream(last: Text.Offset, stack: List[(Text.Info[A], Stream[(Text.Range, Branches.Entry)])])
- : Stream[Text.Info[A]] =
+ def stream(
+ last: Text.Offset,
+ stack: List[(Text.Info[Option[A]], Stream[(Text.Range, Branches.Entry)])])
+ : Stream[Text.Info[Option[A]]] =
{
stack match {
case (parent, (range, (info, tree)) #:: more) :: rest =>
@@ -102,7 +106,7 @@
val start = subrange.start
if (result.isDefinedAt(info)) {
- val next = Text.Info(subrange, result(info))
+ val next = Text.Info[Option[A]](subrange, Some(result(info)))
val nexts = stream(start, (next, subtree) :: (parent, more) :: rest)
if (last < start) parent.restrict(Text.Range(last, start)) #:: nexts
else nexts
@@ -117,12 +121,11 @@
case Nil =>
val stop = root_range.stop
- if (last < stop) Stream(Text.Info(Text.Range(last, stop), default))
+ if (last < stop) Stream(Text.Info(Text.Range(last, stop), None))
else Stream.empty
}
}
- stream(root_range.start, List((Text.Info(root_range, default), overlapping(root_range))))
- .iterator
+ stream(root_range.start, List((Text.Info(root_range, None), overlapping(root_range))))
}
def swing_tree(parent: DefaultMutableTreeNode)
--- a/src/Pure/Syntax/lexicon.ML Wed Sep 08 13:30:41 2010 +0100
+++ b/src/Pure/Syntax/lexicon.ML Wed Sep 08 14:46:21 2010 +0200
@@ -66,6 +66,7 @@
val terminals: string list
val is_terminal: string -> bool
val report_token: Proof.context -> token -> unit
+ val report_token_range: Proof.context -> token -> unit
val matching_tokens: token * token -> bool
val valued_token: token -> bool
val predef_term: string -> token option
@@ -188,6 +189,11 @@
fun report_token ctxt (Token (kind, _, (pos, _))) =
Context_Position.report ctxt (token_kind_markup kind) pos;
+fun report_token_range ctxt tok =
+ if is_proper tok
+ then Context_Position.report ctxt Markup.token_range (pos_of_token tok)
+ else ();
+
(* matching_tokens *)
--- a/src/Pure/Syntax/syntax.ML Wed Sep 08 13:30:41 2010 +0100
+++ b/src/Pure/Syntax/syntax.ML Wed Sep 08 14:46:21 2010 +0200
@@ -709,7 +709,8 @@
val _ = List.app (Lexicon.report_token ctxt) toks;
val root' = if root <> "prop" andalso is_logtype root then Syn_Ext.logic else root;
- val pts = Parser.parse ctxt gram root' (filter Lexicon.is_proper toks);
+ val pts = Parser.parse ctxt gram root' (filter Lexicon.is_proper toks)
+ handle ERROR msg => (List.app (Lexicon.report_token_range ctxt) toks; error msg);
val len = length pts;
val limit = Config.get ctxt ambiguity_limit;
--- a/src/Tools/jEdit/dist-template/properties/jedit.props Wed Sep 08 13:30:41 2010 +0100
+++ b/src/Tools/jEdit/dist-template/properties/jedit.props Wed Sep 08 14:46:21 2010 +0200
@@ -177,6 +177,7 @@
end.shortcut=
fallbackEncodings=UTF-8 ISO-8859-15 US-ASCII
firstTime=false
+foldPainter=Circle
home.shortcut=
insert-newline-indent.shortcut=
insert-newline.shortcut=ENTER
@@ -203,6 +204,7 @@
view.fontsize=18
view.fracFontMetrics=false
view.gutter.fontsize=12
+view.gutter.selectionAreaWidth=18
view.height=787
view.middleMousePaste=true
view.showToolbar=false
--- a/src/Tools/jEdit/src/jedit/document_model.scala Wed Sep 08 13:30:41 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_model.scala Wed Sep 08 14:46:21 2010 +0200
@@ -69,87 +69,6 @@
case _ => false
}
}
-
-
- /* mapping to jEdit token types */
- // TODO: as properties or CSS style sheet
-
- val command_style: Map[String, Byte] =
- {
- import Token._
- Map[String, Byte](
- Keyword.THY_END -> KEYWORD2,
- Keyword.THY_SCRIPT -> LABEL,
- Keyword.PRF_SCRIPT -> LABEL,
- Keyword.PRF_ASM -> KEYWORD3,
- Keyword.PRF_ASM_GOAL -> KEYWORD3
- ).withDefaultValue(KEYWORD1)
- }
-
- val token_style: Map[String, Byte] =
- {
- import Token._
- Map[String, Byte](
- // logical entities
- Markup.TCLASS -> NULL,
- Markup.TYCON -> NULL,
- Markup.FIXED_DECL -> FUNCTION,
- Markup.FIXED -> NULL,
- Markup.CONST_DECL -> FUNCTION,
- Markup.CONST -> NULL,
- Markup.FACT_DECL -> FUNCTION,
- Markup.FACT -> NULL,
- Markup.DYNAMIC_FACT -> LABEL,
- Markup.LOCAL_FACT_DECL -> FUNCTION,
- Markup.LOCAL_FACT -> NULL,
- // inner syntax
- Markup.TFREE -> NULL,
- Markup.FREE -> NULL,
- Markup.TVAR -> NULL,
- Markup.SKOLEM -> NULL,
- Markup.BOUND -> NULL,
- Markup.VAR -> NULL,
- Markup.NUM -> DIGIT,
- Markup.FLOAT -> DIGIT,
- Markup.XNUM -> DIGIT,
- Markup.XSTR -> LITERAL4,
- Markup.LITERAL -> OPERATOR,
- Markup.INNER_COMMENT -> COMMENT1,
- Markup.SORT -> NULL,
- Markup.TYP -> NULL,
- Markup.TERM -> NULL,
- Markup.PROP -> NULL,
- Markup.ATTRIBUTE -> NULL,
- Markup.METHOD -> NULL,
- // ML syntax
- Markup.ML_KEYWORD -> KEYWORD1,
- Markup.ML_DELIMITER -> OPERATOR,
- Markup.ML_IDENT -> NULL,
- Markup.ML_TVAR -> NULL,
- Markup.ML_NUMERAL -> DIGIT,
- Markup.ML_CHAR -> LITERAL1,
- Markup.ML_STRING -> LITERAL1,
- Markup.ML_COMMENT -> COMMENT1,
- Markup.ML_MALFORMED -> INVALID,
- // embedded source text
- Markup.ML_SOURCE -> COMMENT3,
- Markup.DOC_SOURCE -> COMMENT3,
- Markup.ANTIQ -> COMMENT4,
- Markup.ML_ANTIQ -> COMMENT4,
- Markup.DOC_ANTIQ -> COMMENT4,
- // outer syntax
- Markup.KEYWORD -> KEYWORD2,
- Markup.OPERATOR -> OPERATOR,
- Markup.COMMAND -> KEYWORD1,
- Markup.IDENT -> NULL,
- Markup.VERBATIM -> COMMENT3,
- Markup.COMMENT -> COMMENT1,
- Markup.CONTROL -> COMMENT3,
- Markup.MALFORMED -> INVALID,
- Markup.STRING -> LITERAL3,
- Markup.ALTSTRING -> LITERAL1
- ).withDefaultValue(NULL)
- }
}
@@ -272,27 +191,18 @@
handler.handleToken(line_segment, style, offset, length, context)
val syntax = session.current_syntax()
- val token_markup: PartialFunction[Text.Info[Any], Byte] =
- {
- case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
- if syntax.keyword_kind(name).isDefined =>
- Document_Model.Token_Markup.command_style(syntax.keyword_kind(name).get)
-
- case Text.Info(_, XML.Elem(Markup(name, _), _))
- if Document_Model.Token_Markup.token_style(name) != Token.NULL =>
- Document_Model.Token_Markup.token_style(name)
- }
+ val tokens = snapshot.select_markup(Text.Range(start, stop))(Isabelle_Markup.tokens(syntax))
var last = start
- for (token <- snapshot.select_markup(Text.Range(start, stop))(token_markup)(Token.NULL)) {
+ for (token <- tokens.iterator) {
val Text.Range(token_start, token_stop) = token.range
if (last < token_start)
handle_token(Token.COMMENT1, last - start, token_start - last)
- handle_token(token.info, token_start - start, token_stop - token_start)
+ handle_token(token.info getOrElse Token.NULL,
+ token_start - start, token_stop - token_start)
last = token_stop
}
- if (last < stop)
- handle_token(Token.COMMENT1, last - start, stop - last)
+ if (last < stop) handle_token(Token.COMMENT1, last - start, stop - last)
handle_token(Token.END, line_segment.count, 0)
handler.setLineContext(context)
--- a/src/Tools/jEdit/src/jedit/document_view.scala Wed Sep 08 13:30:41 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Wed Sep 08 14:46:21 2010 +0200
@@ -13,42 +13,19 @@
import scala.actors.Actor._
import java.awt.event.{MouseAdapter, MouseMotionAdapter, MouseEvent, FocusAdapter, FocusEvent}
-import java.awt.{BorderLayout, Graphics, Dimension, Color, Graphics2D}
+import java.awt.{BorderLayout, Graphics, Color, Dimension, Graphics2D}
import javax.swing.{JPanel, ToolTipManager}
import javax.swing.event.{CaretListener, CaretEvent}
-import org.gjt.sp.jedit.OperatingSystem
+import org.gjt.sp.jedit.{jEdit, OperatingSystem}
import org.gjt.sp.jedit.gui.RolloverButton
+import org.gjt.sp.jedit.options.GutterOptionPane
import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
import org.gjt.sp.jedit.syntax.SyntaxStyle
object Document_View
{
- /* physical rendering */
-
- def status_color(snapshot: Document.Snapshot, command: Command): Color =
- {
- val state = snapshot.state(command)
- if (snapshot.is_outdated) new Color(240, 240, 240)
- else
- Isar_Document.command_status(state.status) match {
- case Isar_Document.Forked(i) if i > 0 => new Color(255, 228, 225)
- case Isar_Document.Finished => new Color(234, 248, 255)
- case Isar_Document.Failed => new Color(255, 193, 193)
- case Isar_Document.Unprocessed => new Color(255, 228, 225)
- case _ => Color.red
- }
- }
-
- val message_markup: PartialFunction[Text.Info[Any], Color] =
- {
- case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => new Color(220, 220, 220)
- case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => new Color(255, 165, 0)
- case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => new Color(255, 106, 106)
- }
-
-
/* document view of text area */
private val key = new Object
@@ -171,19 +148,17 @@
/* subexpression highlighting */
- private def subexp_range(snapshot: Document.Snapshot, x: Int, y: Int): Option[Text.Range] =
+ private def subexp_range(snapshot: Document.Snapshot, x: Int, y: Int)
+ : Option[(Text.Range, Color)] =
{
- val subexp_markup: PartialFunction[Text.Info[Any], Option[Text.Range]] =
- {
- case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), _)) =>
- Some(snapshot.convert(range))
+ val offset = text_area.xyToOffset(x, y)
+ snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.subexp) match {
+ case Text.Info(_, Some((range, color))) #:: _ => Some((snapshot.convert(range), color))
+ case _ => None
}
- val offset = text_area.xyToOffset(x, y)
- val markup = snapshot.select_markup(Text.Range(offset, offset + 1))(subexp_markup)(None)
- if (markup.hasNext) markup.next.info else None
}
- private var highlight_range: Option[Text.Range] = None
+ private var highlight_range: Option[(Text.Range, Color)] = None
private val focus_listener = new FocusAdapter {
override def focusLost(e: FocusEvent) { highlight_range = None }
@@ -195,10 +170,10 @@
if (!model.buffer.isLoaded) highlight_range = None
else
Isabelle.swing_buffer_lock(model.buffer) {
- highlight_range.map(invalidate_line_range(_))
+ highlight_range map { case (range, _) => invalidate_line_range(range) }
highlight_range =
if (control) subexp_range(model.snapshot(), e.getX(), e.getY()) else None
- highlight_range.map(invalidate_line_range(_))
+ highlight_range map { case (range, _) => invalidate_line_range(range) }
}
}
}
@@ -217,53 +192,70 @@
val saved_color = gfx.getColor
val ascent = text_area.getPainter.getFontMetrics.getAscent
- try {
- for (i <- 0 until physical_lines.length) {
- if (physical_lines(i) != -1) {
- val line_range = proper_line_range(start(i), end(i))
+ for (i <- 0 until physical_lines.length) {
+ if (physical_lines(i) != -1) {
+ val line_range = proper_line_range(start(i), end(i))
- // background color
- val cmds = snapshot.node.command_range(snapshot.revert(line_range))
- for {
- (command, command_start) <- cmds if !command.is_ignored
- val range = line_range.restrict(snapshot.convert(command.range + command_start))
- r <- Isabelle.gfx_range(text_area, range)
- } {
- gfx.setColor(Document_View.status_color(snapshot, command))
- gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
- }
+ // background color: status
+ val cmds = snapshot.node.command_range(snapshot.revert(line_range))
+ for {
+ (command, command_start) <- cmds if !command.is_ignored
+ val range = line_range.restrict(snapshot.convert(command.range + command_start))
+ r <- Isabelle.gfx_range(text_area, range)
+ color <- Isabelle_Markup.status_color(snapshot, command)
+ } {
+ gfx.setColor(color)
+ gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
+ }
+
+ // background color: markup
+ for {
+ Text.Info(range, Some(color)) <-
+ snapshot.select_markup(line_range)(Isabelle_Markup.background).iterator
+ r <- Isabelle.gfx_range(text_area, range)
+ } {
+ gfx.setColor(color)
+ gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
+ }
- // subexpression highlighting -- potentially from other snapshot
- if (highlight_range.isDefined) {
- if (line_range.overlaps(highlight_range.get)) {
- Isabelle.gfx_range(text_area, line_range.restrict(highlight_range.get)) match {
- case None =>
- case Some(r) =>
- gfx.setColor(Color.black)
- gfx.drawRect(r.x, y + i * line_height, r.length, line_height - 1)
- }
+ // sub-expression highlighting -- potentially from other snapshot
+ highlight_range match {
+ case Some((range, color)) if line_range.overlaps(range) =>
+ Isabelle.gfx_range(text_area, line_range.restrict(range)) match {
+ case None =>
+ case Some(r) =>
+ gfx.setColor(color)
+ gfx.drawRect(r.x, y + i * line_height, r.length, line_height - 1)
}
- }
+ case _ =>
+ }
- // squiggly underline
- for {
- Text.Info(range, color) <-
- snapshot.select_markup(line_range)(Document_View.message_markup)(null)
- if color != null
- r <- Isabelle.gfx_range(text_area, range)
- } {
- gfx.setColor(color)
- val x0 = (r.x / 2) * 2
- val y0 = r.y + ascent + 1
- for (x1 <- Range(x0, x0 + r.length, 2)) {
- val y1 = if (x1 % 4 < 2) y0 else y0 + 1
- gfx.drawLine(x1, y1, x1 + 1, y1)
- }
+ // boxed text
+ for {
+ Text.Info(range, Some(color)) <-
+ snapshot.select_markup(line_range)(Isabelle_Markup.box).iterator
+ r <- Isabelle.gfx_range(text_area, range)
+ } {
+ gfx.setColor(color)
+ gfx.drawRect(r.x + 1, y + i * line_height + 1, r.length - 2, line_height - 3)
+ }
+
+ // squiggly underline
+ for {
+ Text.Info(range, Some(color)) <-
+ snapshot.select_markup(line_range)(Isabelle_Markup.message).iterator
+ r <- Isabelle.gfx_range(text_area, range)
+ } {
+ gfx.setColor(color)
+ val x0 = (r.x / 2) * 2
+ val y0 = r.y + ascent + 1
+ for (x1 <- Range(x0, x0 + r.length, 2)) {
+ val y1 = if (x1 % 4 < 2) y0 else y0 + 1
+ gfx.drawLine(x1, y1, x1 + 1, y1)
}
}
}
}
- finally { gfx.setColor(saved_color) }
}
}
@@ -272,12 +264,52 @@
Isabelle.swing_buffer_lock(model.buffer) {
val snapshot = model.snapshot()
val offset = text_area.xyToOffset(x, y)
- val markup =
- snapshot.select_markup(Text.Range(offset, offset + 1)) {
- case Text.Info(range, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
- Isabelle.tooltip(Pretty.string_of(List(Pretty.block(body)), margin = 40))
- } { null }
- if (markup.hasNext) markup.next.info else null
+ snapshot.select_markup(Text.Range(offset, offset + 1))(Isabelle_Markup.tooltip) match
+ {
+ case Text.Info(_, Some(text)) #:: _ => Isabelle.tooltip(text)
+ case _ => null
+ }
+ }
+ }
+ }
+
+
+ /* gutter_extension */
+
+ private val gutter_extension = new TextAreaExtension
+ {
+ override def paintScreenLineRange(gfx: Graphics2D,
+ first_line: Int, last_line: Int, physical_lines: Array[Int],
+ start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+ {
+ val gutter = text_area.getGutter
+ val width = GutterOptionPane.getSelectionAreaWidth
+ val border_width = jEdit.getIntegerProperty("view.gutter.borderWidth", 3)
+ val FOLD_MARKER_SIZE = 12
+
+ if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
+ Isabelle.swing_buffer_lock(model.buffer) {
+ val snapshot = model.snapshot()
+ for (i <- 0 until physical_lines.length) {
+ if (physical_lines(i) != -1) {
+ val line_range = proper_line_range(start(i), end(i))
+
+ // gutter icons
+ val icons =
+ (for (Text.Info(_, Some(icon)) <-
+ snapshot.select_markup(line_range)(Isabelle_Markup.gutter_message).iterator)
+ yield icon).toList.sortWith(_ >= _)
+ icons match {
+ case icon :: _ =>
+ val icn = icon.icon
+ val x0 = (FOLD_MARKER_SIZE + width - border_width - icn.getIconWidth) max 10
+ val y0 = y + i * line_height + (((line_height - icn.getIconHeight) / 2) max 0)
+ icn.paintIcon(gutter, gfx, x0, y0)
+ case Nil =>
+ }
+ }
+ }
+ }
}
}
}
@@ -328,13 +360,6 @@
super.removeNotify
}
- override def getToolTipText(event: MouseEvent): String =
- {
- val line = y_to_line(event.getY())
- if (line >= 0 && line < text_area.getLineCount) "<html><b>TODO:</b><br>Tooltip</html>"
- else ""
- }
-
override def paintComponent(gfx: Graphics)
{
super.paintComponent(gfx)
@@ -342,18 +367,18 @@
val buffer = model.buffer
Isabelle.buffer_lock(buffer) {
val snapshot = model.snapshot()
- val saved_color = gfx.getColor // FIXME needed!?
- try {
- for ((command, start) <- snapshot.node.command_starts if !command.is_ignored) {
- val line1 = buffer.getLineOfOffset(snapshot.convert(start))
- val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
- val y = line_to_y(line1)
- val height = HEIGHT * (line2 - line1)
- gfx.setColor(Document_View.status_color(snapshot, command))
- gfx.fillRect(0, y, getWidth - 1, height)
- }
+ for {
+ (command, start) <- snapshot.node.command_starts
+ if !command.is_ignored
+ val line1 = buffer.getLineOfOffset(snapshot.convert(start))
+ val line2 = buffer.getLineOfOffset(snapshot.convert(start + command.length)) + 1
+ val y = line_to_y(line1)
+ val height = HEIGHT * (line2 - line1)
+ color <- Isabelle_Markup.overview_color(snapshot, command)
+ } {
+ gfx.setColor(color)
+ gfx.fillRect(0, y, getWidth - 1, height)
}
- finally { gfx.setColor(saved_color) }
}
}
@@ -371,6 +396,7 @@
{
text_area.getPainter.
addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, text_area_extension)
+ text_area.getGutter.addExtension(gutter_extension)
text_area.addFocusListener(focus_listener)
text_area.getPainter.addMouseMotionListener(mouse_motion_listener)
text_area.addCaretListener(caret_listener)
@@ -385,6 +411,7 @@
text_area.getPainter.removeMouseMotionListener(mouse_motion_listener)
text_area.removeCaretListener(caret_listener)
text_area.removeLeftOfScrollBar(overview)
+ text_area.getGutter.removeExtension(gutter_extension)
text_area.getPainter.removeExtension(text_area_extension)
}
}
\ No newline at end of file
--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Wed Sep 08 13:30:41 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala Wed Sep 08 14:46:21 2010 +0200
@@ -72,9 +72,11 @@
case _ => null
}
}
- } { null }
- if (markup.hasNext) markup.next.info else null
-
+ }
+ markup match {
+ case Text.Info(_, Some(link)) #:: _ => link
+ case _ => null
+ }
case None => null
}
}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit/isabelle_markup.scala Wed Sep 08 14:46:21 2010 +0200
@@ -0,0 +1,198 @@
+/* Title: Tools/jEdit/src/jedit/isabelle_markup.scala
+ Author: Makarius
+
+Isabelle specific physical rendering and markup selection.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.Color
+
+import org.gjt.sp.jedit.GUIUtilities
+import org.gjt.sp.jedit.syntax.Token
+
+
+object Isabelle_Markup
+{
+ /* physical rendering */
+
+ val outdated_color = new Color(240, 240, 240)
+ val unfinished_color = new Color(255, 228, 225)
+
+ val regular_color = new Color(192, 192, 192)
+ val warning_color = new Color(255, 168, 0)
+ val error_color = new Color(255, 80, 80)
+ val bad_color = new Color(255, 204, 153, 100)
+
+ class Icon(val priority: Int, val icon: javax.swing.Icon)
+ {
+ def >= (that: Icon): Boolean = this.priority >= that.priority
+ }
+ val warning_icon = new Icon(1, GUIUtilities.loadIcon("16x16/status/dialog-warning.png"))
+ val error_icon = new Icon(2, GUIUtilities.loadIcon("16x16/status/dialog-error.png"))
+
+
+ /* command status */
+
+ def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
+ {
+ val state = snapshot.state(command)
+ if (snapshot.is_outdated) Some(outdated_color)
+ else
+ Isar_Document.command_status(state.status) match {
+ case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
+ case Isar_Document.Unprocessed => Some(unfinished_color)
+ case _ => None
+ }
+ }
+
+ def overview_color(snapshot: Document.Snapshot, command: Command): Option[Color] =
+ {
+ val state = snapshot.state(command)
+ if (snapshot.is_outdated) None
+ else
+ Isar_Document.command_status(state.status) match {
+ case Isar_Document.Forked(i) if i > 0 => Some(unfinished_color)
+ case Isar_Document.Unprocessed => Some(unfinished_color)
+ case Isar_Document.Failed => Some(error_color)
+ case _ => None
+ }
+ }
+
+
+ /* markup selectors */
+
+ private val subexp_include =
+ Set(Markup.SORT, Markup.TYP, Markup.TERM, Markup.PROP, Markup.ML_TYPING)
+
+ val subexp: Markup_Tree.Select[(Text.Range, Color)] =
+ {
+ case Text.Info(range, XML.Elem(Markup(name, _), _)) if subexp_include(name) =>
+ (range, Color.black)
+ }
+
+ val message: Markup_Tree.Select[Color] =
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.WRITELN, _), _)) => regular_color
+ case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_color
+ case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color
+ }
+
+ val gutter_message: Markup_Tree.Select[Icon] =
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.WARNING, _), _)) => warning_icon
+ case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_icon
+ }
+
+ val background: Markup_Tree.Select[Color] =
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color
+ }
+
+ val box: Markup_Tree.Select[Color] =
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => regular_color
+ }
+
+ val tooltip: Markup_Tree.Select[String] =
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.ML_TYPING, _), body)) =>
+ Pretty.string_of(List(Pretty.block(body)), margin = 40)
+ case Text.Info(_, XML.Elem(Markup(Markup.SORT, _), _)) => "sort"
+ case Text.Info(_, XML.Elem(Markup(Markup.TYP, _), _)) => "type"
+ case Text.Info(_, XML.Elem(Markup(Markup.TERM, _), _)) => "term"
+ case Text.Info(_, XML.Elem(Markup(Markup.PROP, _), _)) => "proposition"
+ }
+
+
+ /* token markup -- text styles */
+
+ private val command_style: Map[String, Byte] =
+ {
+ import Token._
+ Map[String, Byte](
+ Keyword.THY_END -> KEYWORD2,
+ Keyword.THY_SCRIPT -> LABEL,
+ Keyword.PRF_SCRIPT -> LABEL,
+ Keyword.PRF_ASM -> KEYWORD3,
+ Keyword.PRF_ASM_GOAL -> KEYWORD3
+ ).withDefaultValue(KEYWORD1)
+ }
+
+ private val token_style: Map[String, Byte] =
+ {
+ import Token._
+ Map[String, Byte](
+ // logical entities
+ Markup.TCLASS -> NULL,
+ Markup.TYCON -> NULL,
+ Markup.FIXED_DECL -> FUNCTION,
+ Markup.FIXED -> NULL,
+ Markup.CONST_DECL -> FUNCTION,
+ Markup.CONST -> NULL,
+ Markup.FACT_DECL -> FUNCTION,
+ Markup.FACT -> NULL,
+ Markup.DYNAMIC_FACT -> LABEL,
+ Markup.LOCAL_FACT_DECL -> FUNCTION,
+ Markup.LOCAL_FACT -> NULL,
+ // inner syntax
+ Markup.TFREE -> NULL,
+ Markup.FREE -> NULL,
+ Markup.TVAR -> NULL,
+ Markup.SKOLEM -> NULL,
+ Markup.BOUND -> NULL,
+ Markup.VAR -> NULL,
+ Markup.NUM -> DIGIT,
+ Markup.FLOAT -> DIGIT,
+ Markup.XNUM -> DIGIT,
+ Markup.XSTR -> LITERAL4,
+ Markup.LITERAL -> OPERATOR,
+ Markup.INNER_COMMENT -> COMMENT1,
+ Markup.SORT -> NULL,
+ Markup.TYP -> NULL,
+ Markup.TERM -> NULL,
+ Markup.PROP -> NULL,
+ Markup.ATTRIBUTE -> NULL,
+ Markup.METHOD -> NULL,
+ // ML syntax
+ Markup.ML_KEYWORD -> KEYWORD1,
+ Markup.ML_DELIMITER -> OPERATOR,
+ Markup.ML_IDENT -> NULL,
+ Markup.ML_TVAR -> NULL,
+ Markup.ML_NUMERAL -> DIGIT,
+ Markup.ML_CHAR -> LITERAL1,
+ Markup.ML_STRING -> LITERAL1,
+ Markup.ML_COMMENT -> COMMENT1,
+ Markup.ML_MALFORMED -> INVALID,
+ // embedded source text
+ Markup.ML_SOURCE -> COMMENT3,
+ Markup.DOC_SOURCE -> COMMENT3,
+ Markup.ANTIQ -> COMMENT4,
+ Markup.ML_ANTIQ -> COMMENT4,
+ Markup.DOC_ANTIQ -> COMMENT4,
+ // outer syntax
+ Markup.KEYWORD -> KEYWORD2,
+ Markup.OPERATOR -> OPERATOR,
+ Markup.COMMAND -> KEYWORD1,
+ Markup.IDENT -> NULL,
+ Markup.VERBATIM -> COMMENT3,
+ Markup.COMMENT -> COMMENT1,
+ Markup.CONTROL -> COMMENT3,
+ Markup.MALFORMED -> INVALID,
+ Markup.STRING -> LITERAL3,
+ Markup.ALTSTRING -> LITERAL1
+ ).withDefaultValue(NULL)
+ }
+
+ def tokens(syntax: Outer_Syntax): Markup_Tree.Select[Byte] =
+ {
+ case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
+ if syntax.keyword_kind(name).isDefined => command_style(syntax.keyword_kind(name).get)
+
+ case Text.Info(_, XML.Elem(Markup(name, _), _))
+ if token_style(name) != Token.NULL => token_style(name)
+ }
+}
--- a/src/Tools/jEdit/src/jedit/plugin.scala Wed Sep 08 13:30:41 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/plugin.scala Wed Sep 08 14:46:21 2010 +0200
@@ -286,10 +286,9 @@
Isabelle.setup_tooltips()
}
- override def stop()
+ override def stop() // FIXME fragile
{
Isabelle.session.stop() // FIXME dialog!?
Isabelle.session = null
- Isabelle.system = null
}
}