# HG changeset patch # User wenzelm # Date 1283506979 -7200 # Node ID b8b075f80a1bf1b185166ec0b1a93ccff2438169 # Parent 45facd8f358e45225b19c739486d5347bd1bd387# Parent 30f3d9daaa3a7cfc2c2d11e57302b619aab96043 merged; diff -r 45facd8f358e -r b8b075f80a1b src/Pure/General/position.scala --- 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 } } diff -r 45facd8f358e -r b8b075f80a1b src/Pure/Isar/proof_context.ML --- 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; diff -r 45facd8f358e -r b8b075f80a1b src/Pure/PIDE/isar_document.scala --- 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 } } diff -r 45facd8f358e -r b8b075f80a1b src/Tools/jEdit/src/jedit/document_view.scala --- 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) } } diff -r 45facd8f358e -r b8b075f80a1b src/Tools/jEdit/src/jedit/plugin.scala --- 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 =