more markup;
authorwenzelm
Fri, 01 Apr 2016 21:34:17 +0200
changeset 62806 de9bf8171626
parent 62805 42934bdf90ba
child 62807 3c4e9a7937b1
more markup;
src/Pure/PIDE/markup.ML
src/Pure/PIDE/markup.scala
src/Pure/Syntax/syntax_ext.ML
src/Pure/Tools/rail.ML
src/Tools/jEdit/src/rendering.scala
--- a/src/Pure/PIDE/markup.ML	Fri Apr 01 19:01:34 2016 +0200
+++ b/src/Pure/PIDE/markup.ML	Fri Apr 01 21:34:17 2016 +0200
@@ -61,7 +61,7 @@
   val position_properties': string list
   val position_properties: string list
   val positionN: string val position: T
-  val expressionN: string val expression: T
+  val expressionN: string val expression: string -> T
   val citationN: string val citation: string -> T
   val pathN: string val path: string -> T
   val urlN: string val url: string -> T
@@ -379,7 +379,8 @@
 
 (* expression *)
 
-val (expressionN, expression) = markup_elem "expression";
+val expressionN = "expression";
+fun expression kind = (expressionN, if kind = "" then [] else [(kindN, kind)]);
 
 
 (* citation *)
--- a/src/Pure/PIDE/markup.scala	Fri Apr 01 19:01:34 2016 +0200
+++ b/src/Pure/PIDE/markup.scala	Fri Apr 01 21:34:17 2016 +0200
@@ -131,6 +131,15 @@
   /* expression */
 
   val EXPRESSION = "expression"
+  object Expression
+  {
+    def unapply(markup: Markup): Option[String] =
+      markup match {
+        case Markup(EXPRESSION, Kind(kind)) => Some(kind)
+        case Markup(EXPRESSION, _) => Some("")
+        case _ => None
+      }
+  }
 
 
   /* citation */
--- a/src/Pure/Syntax/syntax_ext.ML	Fri Apr 01 19:01:34 2016 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Fri Apr 01 21:34:17 2016 +0200
@@ -110,15 +110,6 @@
     fold (fn Delim s => insert (op =) s | _ => I) xsymbs) xprods []
   |> map Symbol.explode;
 
-fun reports_of (xsym, pos: Position.T) =
-  (pos, Markup.expression) ::
-    (case xsym of
-      Delim _ => [(pos, Markup.literal)]
-    | Bg _ => [(pos, Markup.keyword3)]
-    | Brk _ => [(pos, Markup.keyword3)]
-    | En => [(pos, Markup.keyword3)]
-    | _ => []);
-
 
 
 (** datatype mfix **)
@@ -210,6 +201,18 @@
 fun scan_many pred = Scan.many (pred o Symbol_Pos.symbol);
 fun scan_many1 pred = Scan.many1 (pred o Symbol_Pos.symbol);
 
+fun reports_of_block pos =
+  [(pos, Markup.expression "mixfix block begin"), (pos, Markup.keyword3)];
+
+fun reports_of (xsym, pos: Position.T) =
+  (case xsym of
+    Delim _ => [(pos, Markup.expression "mixfix delimiter"), (pos, Markup.literal)]
+  | Argument _ => [(pos, Markup.expression "mixfix argument")]
+  | Space _ => [(pos, Markup.expression "mixfix space")]
+  | Bg _ => reports_of_block pos
+  | Brk _ => [(pos, Markup.expression "mixfix break"), (pos, Markup.keyword3)]
+  | En => [(pos, Markup.expression "mixfix block end"), (pos, Markup.keyword3)]);
+
 fun read_block_properties ss =
   let
     val props = read_properties ss;
@@ -227,8 +230,12 @@
     val unbreakable = get_bool Markup.unbreakableN props;
     val indent = get_nat Markup.indentN props;
   in Bg {markup = markup, consistent = consistent, unbreakable = unbreakable, indent = indent} end
-  handle ERROR msg => error (msg ^
-    Markup.markup_report (Position.reported_text (#1 (Symbol_Pos.range ss)) Markup.keyword3 ""));
+  handle ERROR msg =>
+    let
+      val reported_texts =
+        reports_of_block (#1 (Symbol_Pos.range ss))
+        |> map (fn (p, m) => Markup.markup_report (Position.reported_text p m ""))
+    in error (msg ^ implode reported_texts) end;
 
 val read_block_indent =
   Bg o block_indent o #1 o Library.read_int o map Symbol_Pos.symbol;
--- a/src/Pure/Tools/rail.ML	Fri Apr 01 19:01:34 2016 +0200
+++ b/src/Pure/Tools/rail.ML	Fri Apr 01 21:34:17 2016 +0200
@@ -188,7 +188,7 @@
     let
       fun reports r =
         if r = Position.no_range then []
-        else [(Position.range_position r, Markup.expression)];
+        else [(Position.range_position r, Markup.expression "")];
       fun trees (CAT (ts, r)) = reports r @ maps tree ts
       and tree (BAR (Ts, r)) = reports r @ maps trees Ts
         | tree (STAR ((T1, T2), r)) = reports r @ trees T1 @ trees T2
--- a/src/Tools/jEdit/src/rendering.scala	Fri Apr 01 19:01:34 2016 +0200
+++ b/src/Tools/jEdit/src/rendering.scala	Fri Apr 01 21:34:17 2016 +0200
@@ -172,7 +172,6 @@
 
   private val tooltip_descriptions =
     Map(
-      Markup.EXPRESSION -> "expression",
       Markup.CITATION -> "citation",
       Markup.TOKEN_RANGE -> "inner syntax token",
       Markup.FREE -> "free variable",
@@ -183,9 +182,9 @@
       Markup.TVAR -> "schematic type variable")
 
   private val tooltip_elements =
-    Markup.Elements(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
-      Markup.TYPING, Markup.ML_TYPING, Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC,
-      Markup.URL, Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name) ++
+    Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
+      Markup.SORTING, Markup.TYPING, Markup.ML_TYPING, Markup.ML_BREAKPOINT, Markup.PATH,
+      Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name) ++
     Markup.Elements(tooltip_descriptions.keySet)
 
   private val gutter_elements =
@@ -567,10 +566,15 @@
               if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
               else "breakpoint (disabled)"
             Some(add(prev, r, (true, XML.Text(text))))
+
           case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
             val lang = Word.implode(Word.explode('_', language))
             Some(add(prev, r, (true, XML.Text("language: " + lang))))
 
+          case (prev, Text.Info(r, XML.Elem(Markup.Expression(kind), _))) =>
+            val descr = if (kind == "") "expression" else "expression: " + kind
+            Some(add(prev, r, (true, XML.Text(descr))))
+
           case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
             Some(add(prev, r, (true, XML.Text("Markdown: paragraph"))))
           case (prev, Text.Info(r, XML.Elem(Markup.Markdown_List(kind), _))) =>