# HG changeset patch # User wenzelm # Date 1459539257 -7200 # Node ID de9bf817162614352649053283e70da95e608e09 # Parent 42934bdf90bacb51117507a6da967574f0897bc7 more markup; diff -r 42934bdf90ba -r de9bf8171626 src/Pure/PIDE/markup.ML --- 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 *) diff -r 42934bdf90ba -r de9bf8171626 src/Pure/PIDE/markup.scala --- 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 */ diff -r 42934bdf90ba -r de9bf8171626 src/Pure/Syntax/syntax_ext.ML --- 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; diff -r 42934bdf90ba -r de9bf8171626 src/Pure/Tools/rail.ML --- 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 diff -r 42934bdf90ba -r de9bf8171626 src/Tools/jEdit/src/rendering.scala --- 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), _))) =>