# HG changeset patch # User wenzelm # Date 1284736244 -7200 # Node ID 4110cc1b8f9f135d88ae15590ee30e68c3d29360 # Parent 4c2547af5909a3a5bb7bc65491a37c9fa9fb8815 allow embedded reports in regular prover messages, to avoid side-effects for errors for example; diff -r 4c2547af5909 -r 4110cc1b8f9f src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Fri Sep 17 17:09:31 2010 +0200 +++ b/src/Pure/Isar/proof_context.ML Fri Sep 17 17:10:44 2010 +0200 @@ -734,8 +734,8 @@ local fun parse_failed ctxt pos msg kind = - (Context_Position.report ctxt Markup.bad pos; - cat_error msg ("Failed to parse " ^ kind)); + cat_error msg ("Failed to parse " ^ kind ^ + Markup.markup Markup.report (Context_Position.reported_text ctxt Markup.bad pos "")); fun parse_sort ctxt text = let diff -r 4c2547af5909 -r 4110cc1b8f9f src/Pure/PIDE/command.scala --- a/src/Pure/PIDE/command.scala Fri Sep 17 17:09:31 2010 +0200 +++ b/src/Pure/PIDE/command.scala Fri Sep 17 17:10:44 2010 +0200 @@ -60,8 +60,10 @@ 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, message))( - (st, range) => st.add_markup(Text.Info(range, result))) + val st1 = + (add_result(i, result) /: Isar_Document.message_positions(command, message))( + (st, range) => st.add_markup(Text.Info(range, result))) + (st1 /: Isar_Document.message_reports(message))(_ accumulate _) case _ => System.err.println("Ignored message without serial number: " + message); this } } diff -r 4c2547af5909 -r 4110cc1b8f9f src/Pure/PIDE/isar_document.scala --- a/src/Pure/PIDE/isar_document.scala Fri Sep 17 17:09:31 2010 +0200 +++ b/src/Pure/PIDE/isar_document.scala Fri Sep 17 17:10:44 2010 +0200 @@ -56,35 +56,42 @@ } - /* messages */ + /* result messages */ def clean_message(body: XML.Body): XML.Body = body filter { case XML.Elem(Markup(Markup.NO_REPORT, _), _) => false case _ => true } map { case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts)) case t => t } + def message_reports(msg: XML.Tree): List[XML.Elem] = + msg match { + case elem @ XML.Elem(Markup(Markup.REPORT, _), _) => List(elem) + case XML.Elem(_, body) => body.flatMap(message_reports) + case XML.Text(_) => Nil + } + /* reported positions */ - private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION) - - private def is_state(msg: XML.Tree): Boolean = + 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] = + private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION) + + def message_positions(command: Command, message: XML.Elem): Set[Text.Range] = { - def reported(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] = + def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] = tree match { 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) => body.foldLeft(set)(reported) + body.foldLeft(if (range.is_singularity) set else set + range)(positions) + case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(positions) case _ => set } - val set = reported(Set.empty, message) + val set = positions(Set.empty, message) if (set.isEmpty && !is_state(message)) set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_)) else set diff -r 4c2547af5909 -r 4110cc1b8f9f src/Tools/jEdit/dist-template/etc/isabelle-jedit.css --- a/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css Fri Sep 17 17:09:31 2010 +0200 +++ b/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css Fri Sep 17 17:10:44 2010 +0200 @@ -8,6 +8,8 @@ .error { background-color: #FFC1C1; } .debug { background-color: #FFE4E1; } +.report { display: none; } + .hilite { background-color: #FFFACD; } .keyword { font-weight: bold; color: #009966; }