--- 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), _))) =>