# HG changeset patch # User wenzelm # Date 1283868509 -7200 # Node ID 525a13b9ac74b13677911c1893dd4e18fc53f86d # Parent 04ad0fed81f512cc6d7d7cb90490333866918a06 highlight bad range of nested error (here from inner parsing); diff -r 04ad0fed81f5 -r 525a13b9ac74 src/Pure/General/markup.ML --- a/src/Pure/General/markup.ML Tue Sep 07 15:03:59 2010 +0200 +++ b/src/Pure/General/markup.ML Tue Sep 07 16:08:29 2010 +0200 @@ -120,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 @@ -348,6 +349,8 @@ val (reportN, report) = markup_elem "report"; +val (badN, bad) = markup_elem "bad"; + (** print mode operations **) diff -r 04ad0fed81f5 -r 525a13b9ac74 src/Pure/General/markup.scala --- a/src/Pure/General/markup.scala Tue Sep 07 15:03:59 2010 +0200 +++ b/src/Pure/General/markup.scala Tue Sep 07 16:08:29 2010 +0200 @@ -249,6 +249,8 @@ val SIGNAL = "signal" val EXIT = "exit" + val BAD = "bad" + val Ready = Markup("ready", Nil) diff -r 04ad0fed81f5 -r 525a13b9ac74 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Tue Sep 07 15:03:59 2010 +0200 +++ b/src/Pure/Isar/proof_context.ML Tue Sep 07 16:08:29 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; diff -r 04ad0fed81f5 -r 525a13b9ac74 src/Tools/jEdit/src/jedit/document_view.scala --- a/src/Tools/jEdit/src/jedit/document_view.scala Tue Sep 07 15:03:59 2010 +0200 +++ b/src/Tools/jEdit/src/jedit/document_view.scala Tue Sep 07 16:08:29 2010 +0200 @@ -33,6 +33,7 @@ val regular_color = new Color(192, 192, 192) val warning_color = new Color(255, 165, 0) val error_color = new Color(255, 106, 106) + val bad_color = new Color(255, 204, 153, 100) def status_color(snapshot: Document.Snapshot, command: Command): Option[Color] = { @@ -67,6 +68,11 @@ case Text.Info(_, XML.Elem(Markup(Markup.ERROR, _), _)) => error_color } + val background_markup: PartialFunction[Text.Info[Any], Color] = + { + case Text.Info(_, XML.Elem(Markup(Markup.BAD, _), _)) => bad_color + } + val box_markup: PartialFunction[Text.Info[Any], Color] = { case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => regular_color @@ -246,7 +252,7 @@ if (physical_lines(i) != -1) { val line_range = proper_line_range(start(i), end(i)) - // background color + // background color: status val cmds = snapshot.node.command_range(snapshot.revert(line_range)) for { (command, command_start) <- cmds if !command.is_ignored @@ -258,6 +264,17 @@ gfx.fillRect(r.x, y + i * line_height, r.length, line_height) } + // background color: markup + for { + Text.Info(range, color) <- + snapshot.select_markup(line_range)(Document_View.background_markup)(null) + if color != null + 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)) {