more markup;
authorwenzelm
Fri Apr 01 21:34:17 2016 +0200 (2016-04-01)
changeset 62806de9bf8171626
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
     1.1 --- a/src/Pure/PIDE/markup.ML	Fri Apr 01 19:01:34 2016 +0200
     1.2 +++ b/src/Pure/PIDE/markup.ML	Fri Apr 01 21:34:17 2016 +0200
     1.3 @@ -61,7 +61,7 @@
     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 expressionN: string val expression: T
     1.8 +  val expressionN: string val expression: string -> T
     1.9    val citationN: string val citation: string -> T
    1.10    val pathN: string val path: string -> T
    1.11    val urlN: string val url: string -> T
    1.12 @@ -379,7 +379,8 @@
    1.13  
    1.14  (* expression *)
    1.15  
    1.16 -val (expressionN, expression) = markup_elem "expression";
    1.17 +val expressionN = "expression";
    1.18 +fun expression kind = (expressionN, if kind = "" then [] else [(kindN, kind)]);
    1.19  
    1.20  
    1.21  (* citation *)
     2.1 --- a/src/Pure/PIDE/markup.scala	Fri Apr 01 19:01:34 2016 +0200
     2.2 +++ b/src/Pure/PIDE/markup.scala	Fri Apr 01 21:34:17 2016 +0200
     2.3 @@ -131,6 +131,15 @@
     2.4    /* expression */
     2.5  
     2.6    val EXPRESSION = "expression"
     2.7 +  object Expression
     2.8 +  {
     2.9 +    def unapply(markup: Markup): Option[String] =
    2.10 +      markup match {
    2.11 +        case Markup(EXPRESSION, Kind(kind)) => Some(kind)
    2.12 +        case Markup(EXPRESSION, _) => Some("")
    2.13 +        case _ => None
    2.14 +      }
    2.15 +  }
    2.16  
    2.17  
    2.18    /* citation */
     3.1 --- a/src/Pure/Syntax/syntax_ext.ML	Fri Apr 01 19:01:34 2016 +0200
     3.2 +++ b/src/Pure/Syntax/syntax_ext.ML	Fri Apr 01 21:34:17 2016 +0200
     3.3 @@ -110,15 +110,6 @@
     3.4      fold (fn Delim s => insert (op =) s | _ => I) xsymbs) xprods []
     3.5    |> map Symbol.explode;
     3.6  
     3.7 -fun reports_of (xsym, pos: Position.T) =
     3.8 -  (pos, Markup.expression) ::
     3.9 -    (case xsym of
    3.10 -      Delim _ => [(pos, Markup.literal)]
    3.11 -    | Bg _ => [(pos, Markup.keyword3)]
    3.12 -    | Brk _ => [(pos, Markup.keyword3)]
    3.13 -    | En => [(pos, Markup.keyword3)]
    3.14 -    | _ => []);
    3.15 -
    3.16  
    3.17  
    3.18  (** datatype mfix **)
    3.19 @@ -210,6 +201,18 @@
    3.20  fun scan_many pred = Scan.many (pred o Symbol_Pos.symbol);
    3.21  fun scan_many1 pred = Scan.many1 (pred o Symbol_Pos.symbol);
    3.22  
    3.23 +fun reports_of_block pos =
    3.24 +  [(pos, Markup.expression "mixfix block begin"), (pos, Markup.keyword3)];
    3.25 +
    3.26 +fun reports_of (xsym, pos: Position.T) =
    3.27 +  (case xsym of
    3.28 +    Delim _ => [(pos, Markup.expression "mixfix delimiter"), (pos, Markup.literal)]
    3.29 +  | Argument _ => [(pos, Markup.expression "mixfix argument")]
    3.30 +  | Space _ => [(pos, Markup.expression "mixfix space")]
    3.31 +  | Bg _ => reports_of_block pos
    3.32 +  | Brk _ => [(pos, Markup.expression "mixfix break"), (pos, Markup.keyword3)]
    3.33 +  | En => [(pos, Markup.expression "mixfix block end"), (pos, Markup.keyword3)]);
    3.34 +
    3.35  fun read_block_properties ss =
    3.36    let
    3.37      val props = read_properties ss;
    3.38 @@ -227,8 +230,12 @@
    3.39      val unbreakable = get_bool Markup.unbreakableN props;
    3.40      val indent = get_nat Markup.indentN props;
    3.41    in Bg {markup = markup, consistent = consistent, unbreakable = unbreakable, indent = indent} end
    3.42 -  handle ERROR msg => error (msg ^
    3.43 -    Markup.markup_report (Position.reported_text (#1 (Symbol_Pos.range ss)) Markup.keyword3 ""));
    3.44 +  handle ERROR msg =>
    3.45 +    let
    3.46 +      val reported_texts =
    3.47 +        reports_of_block (#1 (Symbol_Pos.range ss))
    3.48 +        |> map (fn (p, m) => Markup.markup_report (Position.reported_text p m ""))
    3.49 +    in error (msg ^ implode reported_texts) end;
    3.50  
    3.51  val read_block_indent =
    3.52    Bg o block_indent o #1 o Library.read_int o map Symbol_Pos.symbol;
     4.1 --- a/src/Pure/Tools/rail.ML	Fri Apr 01 19:01:34 2016 +0200
     4.2 +++ b/src/Pure/Tools/rail.ML	Fri Apr 01 21:34:17 2016 +0200
     4.3 @@ -188,7 +188,7 @@
     4.4      let
     4.5        fun reports r =
     4.6          if r = Position.no_range then []
     4.7 -        else [(Position.range_position r, Markup.expression)];
     4.8 +        else [(Position.range_position r, Markup.expression "")];
     4.9        fun trees (CAT (ts, r)) = reports r @ maps tree ts
    4.10        and tree (BAR (Ts, r)) = reports r @ maps trees Ts
    4.11          | tree (STAR ((T1, T2), r)) = reports r @ trees T1 @ trees T2
     5.1 --- a/src/Tools/jEdit/src/rendering.scala	Fri Apr 01 19:01:34 2016 +0200
     5.2 +++ b/src/Tools/jEdit/src/rendering.scala	Fri Apr 01 21:34:17 2016 +0200
     5.3 @@ -172,7 +172,6 @@
     5.4  
     5.5    private val tooltip_descriptions =
     5.6      Map(
     5.7 -      Markup.EXPRESSION -> "expression",
     5.8        Markup.CITATION -> "citation",
     5.9        Markup.TOKEN_RANGE -> "inner syntax token",
    5.10        Markup.FREE -> "free variable",
    5.11 @@ -183,9 +182,9 @@
    5.12        Markup.TVAR -> "schematic type variable")
    5.13  
    5.14    private val tooltip_elements =
    5.15 -    Markup.Elements(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
    5.16 -      Markup.TYPING, Markup.ML_TYPING, Markup.ML_BREAKPOINT, Markup.PATH, Markup.DOC,
    5.17 -      Markup.URL, Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name) ++
    5.18 +    Markup.Elements(Markup.LANGUAGE, Markup.EXPRESSION, Markup.TIMING, Markup.ENTITY,
    5.19 +      Markup.SORTING, Markup.TYPING, Markup.ML_TYPING, Markup.ML_BREAKPOINT, Markup.PATH,
    5.20 +      Markup.DOC, Markup.URL, Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name) ++
    5.21      Markup.Elements(tooltip_descriptions.keySet)
    5.22  
    5.23    private val gutter_elements =
    5.24 @@ -567,10 +566,15 @@
    5.25                if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
    5.26                else "breakpoint (disabled)"
    5.27              Some(add(prev, r, (true, XML.Text(text))))
    5.28 +
    5.29            case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
    5.30              val lang = Word.implode(Word.explode('_', language))
    5.31              Some(add(prev, r, (true, XML.Text("language: " + lang))))
    5.32  
    5.33 +          case (prev, Text.Info(r, XML.Elem(Markup.Expression(kind), _))) =>
    5.34 +            val descr = if (kind == "") "expression" else "expression: " + kind
    5.35 +            Some(add(prev, r, (true, XML.Text(descr))))
    5.36 +
    5.37            case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
    5.38              Some(add(prev, r, (true, XML.Text("Markdown: paragraph"))))
    5.39            case (prev, Text.Info(r, XML.Elem(Markup.Markdown_List(kind), _))) =>