eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
authorwenzelm
Fri Sep 17 15:51:11 2010 +0200 (2010-09-17 ago)
changeset 394391c294d150ded
parent 39438 c5ece2a7a86e
child 39440 4c2547af5909
eliminated markup "location" in favour of more explicit "no_report", which is actually deleted from messages;
src/Pure/General/markup.ML
src/Pure/General/markup.scala
src/Pure/Isar/runtime.ML
src/Pure/ML/ml_compiler_polyml-5.3.ML
src/Pure/PIDE/isar_document.scala
src/Pure/System/isabelle_process.scala
src/Tools/jEdit/dist-template/etc/isabelle-jedit.css
     1.1 --- a/src/Pure/General/markup.ML	Thu Sep 16 15:37:12 2010 +0200
     1.2 +++ b/src/Pure/General/markup.ML	Fri Sep 17 15:51:11 2010 +0200
     1.3 @@ -30,7 +30,6 @@
     1.4    val position_properties': string list
     1.5    val position_properties: string list
     1.6    val positionN: string val position: T
     1.7 -  val locationN: string val location: T
     1.8    val indentN: string
     1.9    val blockN: string val block: int -> T
    1.10    val widthN: string
    1.11 @@ -120,6 +119,7 @@
    1.12    val promptN: string val prompt: T
    1.13    val readyN: string val ready: T
    1.14    val reportN: string val report: T
    1.15 +  val no_reportN: string val no_report: T
    1.16    val badN: string val bad: T
    1.17    val no_output: output * output
    1.18    val default_output: T -> output * output
    1.19 @@ -194,7 +194,6 @@
    1.20  val position_properties = [lineN, columnN, offsetN] @ position_properties';
    1.21  
    1.22  val (positionN, position) = markup_elem "position";
    1.23 -val (locationN, location) = markup_elem "location";
    1.24  
    1.25  
    1.26  (* pretty printing *)
    1.27 @@ -348,6 +347,7 @@
    1.28  val (readyN, ready) = markup_elem "ready";
    1.29  
    1.30  val (reportN, report) = markup_elem "report";
    1.31 +val (no_reportN, no_report) = markup_elem "no_report";
    1.32  
    1.33  val (badN, bad) = markup_elem "bad";
    1.34  
     2.1 --- a/src/Pure/General/markup.scala	Thu Sep 16 15:37:12 2010 +0200
     2.2 +++ b/src/Pure/General/markup.scala	Fri Sep 17 15:51:11 2010 +0200
     2.3 @@ -90,7 +90,6 @@
     2.4      Set(LINE, COLUMN, OFFSET, END_LINE, END_COLUMN, END_OFFSET, FILE, ID)
     2.5  
     2.6    val POSITION = "position"
     2.7 -  val LOCATION = "location"
     2.8  
     2.9  
    2.10    /* pretty printing */
    2.11 @@ -236,7 +235,6 @@
    2.12  
    2.13    val INIT = "init"
    2.14    val STATUS = "status"
    2.15 -  val REPORT = "report"
    2.16    val WRITELN = "writeln"
    2.17    val TRACING = "tracing"
    2.18    val WARNING = "warning"
    2.19 @@ -249,6 +247,9 @@
    2.20    val SIGNAL = "signal"
    2.21    val EXIT = "exit"
    2.22  
    2.23 +  val REPORT = "report"
    2.24 +  val NO_REPORT = "no_report"
    2.25 +
    2.26    val BAD = "bad"
    2.27  
    2.28    val Ready = Markup("ready", Nil)
     3.1 --- a/src/Pure/Isar/runtime.ML	Thu Sep 16 15:37:12 2010 +0200
     3.2 +++ b/src/Pure/Isar/runtime.ML	Fri Sep 17 15:51:11 2010 +0200
     3.3 @@ -61,7 +61,7 @@
     3.4            Exn.EXCEPTIONS exns => maps (exn_msgs context) exns
     3.5          | CONTEXT (ctxt, exn) => exn_msgs (SOME ctxt) exn
     3.6          | EXCURSION_FAIL (exn, loc) =>
     3.7 -            map (fn msg => msg ^ Markup.markup Markup.location ("\n" ^ loc)) (exn_msgs context exn)
     3.8 +            map (fn msg => msg ^ Markup.markup Markup.no_report ("\n" ^ loc)) (exn_msgs context exn)
     3.9          | TERMINATE => ["Exit"]
    3.10          | TimeLimit.TimeOut => ["Timeout"]
    3.11          | TOPLEVEL_ERROR => ["Error"]
     4.1 --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Thu Sep 16 15:37:12 2010 +0200
     4.2 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Fri Sep 17 15:51:11 2010 +0200
     4.3 @@ -121,7 +121,7 @@
     4.4      fun message {message = msg, hard, location = loc, context = _} =
     4.5        let
     4.6          val txt =
     4.7 -          Markup.markup Markup.location
     4.8 +          Markup.markup Markup.no_report
     4.9              ((if hard then "Error" else "Warning") ^ Position.str_of (position_of loc) ^ ":\n") ^
    4.10            Pretty.string_of (Pretty.from_ML (pretty_ml msg)) ^
    4.11            Markup.markup (Position.report_markup (offset_position_of loc)) "";
     5.1 --- a/src/Pure/PIDE/isar_document.scala	Thu Sep 16 15:37:12 2010 +0200
     5.2 +++ b/src/Pure/PIDE/isar_document.scala	Fri Sep 17 15:51:11 2010 +0200
     5.3 @@ -56,10 +56,16 @@
     5.4    }
     5.5  
     5.6  
     5.7 +  /* messages */
     5.8 +
     5.9 +  def clean_message(body: XML.Body): XML.Body =
    5.10 +    body filter { case XML.Elem(Markup(Markup.NO_REPORT, _), _) => false case _ => true } map
    5.11 +      { case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts)) case t => t }
    5.12 +
    5.13 +
    5.14    /* reported positions */
    5.15  
    5.16    private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
    5.17 -  private val exclude_pos = Set(Markup.LOCATION)
    5.18  
    5.19    private def is_state(msg: XML.Tree): Boolean =
    5.20      msg match {
    5.21 @@ -75,8 +81,7 @@
    5.22          if include_pos(name) && id == command.id =>
    5.23            val range = command.decode(raw_range).restrict(command.range)
    5.24            body.foldLeft(if (range.is_singularity) set else set + range)(reported)
    5.25 -        case XML.Elem(Markup(name, _), body) if !exclude_pos(name) =>
    5.26 -          body.foldLeft(set)(reported)
    5.27 +        case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(reported)
    5.28          case _ => set
    5.29        }
    5.30      val set = reported(Set.empty, message)
     6.1 --- a/src/Pure/System/isabelle_process.scala	Thu Sep 16 15:37:12 2010 +0200
     6.2 +++ b/src/Pure/System/isabelle_process.scala	Fri Sep 17 15:51:11 2010 +0200
     6.3 @@ -100,7 +100,8 @@
     6.4      if (pid.isEmpty && kind == Markup.INIT)
     6.5        pid = props.find(_._1 == Markup.PID).map(_._1)
     6.6  
     6.7 -    xml_cache.cache_tree(XML.Elem(Markup(kind, props), body))((message: XML.Tree) =>
     6.8 +    val msg = XML.Elem(Markup(kind, props), Isar_Document.clean_message(body))
     6.9 +    xml_cache.cache_tree(msg)((message: XML.Tree) =>
    6.10        receiver ! new Result(message.asInstanceOf[XML.Elem]))
    6.11    }
    6.12  
     7.1 --- a/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Thu Sep 16 15:37:12 2010 +0200
     7.2 +++ b/src/Tools/jEdit/dist-template/etc/isabelle-jedit.css	Fri Sep 17 15:51:11 2010 +0200
     7.3 @@ -8,8 +8,6 @@
     7.4  .error { background-color: #FFC1C1; }
     7.5  .debug { background-color: #FFE4E1; }
     7.6  
     7.7 -.location { display: none; }
     7.8 -
     7.9  .hilite { background-color: #FFFACD; }
    7.10  
    7.11  .keyword { font-weight: bold; color: #009966; }