--- a/src/Pure/General/position.scala Fri Sep 03 11:27:35 2010 +0200
+++ b/src/Pure/General/position.scala Fri Sep 03 11:42:59 2010 +0200
@@ -24,7 +24,7 @@
def unapply(pos: T): Option[Text.Range] =
(Offset.unapply(pos), End_Offset.unapply(pos)) match {
case (Some(start), Some(stop)) if start <= stop => Some(Text.Range(start, stop))
- case (Some(start), None) => Some(Text.Range(start))
+ case (Some(start), None) => Some(Text.Range(start, start + 1))
case _ => None
}
}
--- a/src/Pure/Isar/proof_context.ML Fri Sep 03 11:27:35 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML Fri Sep 03 11:42:59 2010 +0200
@@ -741,14 +741,14 @@
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" ^ Position.str_of pos)
+ handle ERROR msg => cat_error msg "Failed to parse 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" ^ Position.str_of pos);
+ handle ERROR msg => cat_error msg "Failed to parse type";
in T end;
fun parse_term T ctxt text =
@@ -756,7 +756,8 @@
val {get_sort, map_const, map_free} = term_context ctxt;
val (T', _) = Type_Infer.paramify_dummies T 0;
- val (markup, kind) = if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
+ val (markup, kind) =
+ if T' = propT then (Markup.prop, "proposition") else (Markup.term, "term");
val (syms, pos) = Syntax.parse_token ctxt markup text;
fun check t = (Syntax.check_term ctxt (Type_Infer.constrain T' t); NONE)
@@ -764,7 +765,7 @@
val t =
Syntax.standard_parse_term (Syntax.pp ctxt) 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 ^ Position.str_of pos);
+ handle ERROR msg => cat_error msg ("Failed to parse " ^ kind);
in t end;
--- a/src/Pure/PIDE/isar_document.scala Fri Sep 03 11:27:35 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala Fri Sep 03 11:42:59 2010 +0200
@@ -58,17 +58,23 @@
/* reported positions */
+ 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] =
{
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 (name == Markup.BINDING || name == Markup.ENTITY || name == Markup.REPORT) &&
- id == command_id => body.foldLeft(set + range)(reported)
- case XML.Elem(_, body) => body.foldLeft(set)(reported)
- case XML.Text(_) => set
+ if include_pos(name) && id == command_id =>
+ body.foldLeft(set + range)(reported)
+ case XML.Elem(Markup(name, _), body) if !exclude_pos(name) =>
+ body.foldLeft(set)(reported)
+ case _ => set
}
- reported(Set.empty, message) ++ Position.Range.unapply(message.markup.properties)
+ val set = reported(Set.empty, message)
+ if (set.isEmpty) set ++ Position.Range.unapply(message.markup.properties)
+ else set
}
}
--- a/src/Tools/jEdit/src/jedit/document_view.scala Fri Sep 03 11:27:35 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_view.scala Fri Sep 03 11:42:59 2010 +0200
@@ -24,7 +24,9 @@
object Document_View
{
- def choose_color(snapshot: Document.Snapshot, command: Command): Color =
+ /* 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)
@@ -38,6 +40,13 @@
}
}
+ 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 */
@@ -163,18 +172,36 @@
Isabelle.swing_buffer_lock(model.buffer) {
val snapshot = model.snapshot()
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))
+
+ // background color
val cmds = snapshot.node.command_range(snapshot.revert(line_range))
- for ((command, command_start) <- cmds if !command.is_ignored) {
+ for {
+ (command, command_start) <- cmds if !command.is_ignored
val range = line_range.restrict(snapshot.convert(command.range + command_start))
- val p = text_area.offsetToXY(range.start)
- val q = text_area.offsetToXY(range.stop)
- if (p != null && q != null) {
- gfx.setColor(Document_View.choose_color(snapshot, command))
- gfx.fillRect(p.x, y + i * line_height, q.x - p.x, line_height)
+ 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)
+ }
+
+ // 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)
}
}
}
@@ -266,7 +293,7 @@
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.choose_color(snapshot, command))
+ gfx.setColor(Document_View.status_color(snapshot, command))
gfx.fillRect(0, y, getWidth - 1, height)
}
}
--- a/src/Tools/jEdit/src/jedit/plugin.scala Fri Sep 03 11:27:35 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/plugin.scala Fri Sep 03 11:42:59 2010 +0200
@@ -17,7 +17,7 @@
import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, EditPane, ServiceManager, View}
import org.gjt.sp.jedit.buffer.JEditBuffer
-import org.gjt.sp.jedit.textarea.JEditTextArea
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
import org.gjt.sp.jedit.msg.{BufferUpdate, EditPaneUpdate, PropertiesChanged}
import org.gjt.sp.jedit.gui.DockableWindowManager
@@ -74,6 +74,19 @@
Int_Property("relative-font-size", 100)).toFloat / 100
+ /* text area ranges */
+
+ case class Gfx_Range(val x: Int, val y: Int, val length: Int)
+
+ def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
+ {
+ val p = text_area.offsetToXY(range.start)
+ val q = text_area.offsetToXY(range.stop)
+ if (p != null && q != null && p.y == q.y) Some(new Gfx_Range(p.x, p.y, q.x - p.x))
+ else None
+ }
+
+
/* tooltip markup */
def tooltip(text: String): String =