more markup;
authorwenzelm
Thu Oct 15 16:12:38 2015 +0200 (2015-10-15)
changeset 61450239a04ec2d4c
parent 61449 4f31f79cf2d1
child 61451 7f530057bc3c
more markup;
src/Pure/General/antiquote.ML
src/Pure/Thy/markdown.ML
src/Tools/jEdit/src/rendering.scala
     1.1 --- a/src/Pure/General/antiquote.ML	Thu Oct 15 15:06:03 2015 +0200
     1.2 +++ b/src/Pure/General/antiquote.ML	Thu Oct 15 16:12:38 2015 +0200
     1.3 @@ -9,6 +9,7 @@
     1.4    type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range}
     1.5    datatype 'a antiquote = Text of 'a | Antiq of antiq
     1.6    type text_antiquote = Symbol_Pos.T list antiquote
     1.7 +  val range: text_antiquote list -> Position.range
     1.8    val split_lines: text_antiquote list -> text_antiquote list list
     1.9    val antiq_reports: antiq -> Position.report list
    1.10    val antiquote_reports: ('a -> Position.report_text list) ->
    1.11 @@ -28,6 +29,13 @@
    1.12  
    1.13  type text_antiquote = Symbol_Pos.T list antiquote;
    1.14  
    1.15 +fun antiquote_range (Text ss) = Symbol_Pos.range ss
    1.16 +  | antiquote_range (Antiq (_, {range, ...})) = range;
    1.17 +
    1.18 +fun range ants =
    1.19 +  if null ants then Position.no_range
    1.20 +  else Position.range (#1 (antiquote_range (hd ants))) (#2 (antiquote_range (List.last ants)));
    1.21 +
    1.22  
    1.23  (* split lines *)
    1.24  
     2.1 --- a/src/Pure/Thy/markdown.ML	Thu Oct 15 15:06:03 2015 +0200
     2.2 +++ b/src/Pure/Thy/markdown.ML	Thu Oct 15 16:12:38 2015 +0200
     2.3 @@ -104,6 +104,10 @@
     2.4  
     2.5  datatype block = Paragraph of line list | List of marker * block list;
     2.6  
     2.7 +fun block_lines (Paragraph lines) = lines
     2.8 +  | block_lines (List (_, blocks)) = maps block_lines blocks;
     2.9 +
    2.10 +
    2.11  fun add_span (opt_marker, body) document =
    2.12    (case (opt_marker, document) of
    2.13      (SOME marker, (list as List (list_marker, list_body)) :: rest) =>
    2.14 @@ -154,15 +158,22 @@
    2.15  local
    2.16  
    2.17  fun line_reports depth (Line {marker = SOME (_, pos), ...}) =
    2.18 -      Position.is_reported pos ? cons (pos, Markup.markdown_item depth)
    2.19 +      cons (pos, Markup.markdown_item depth)
    2.20    | line_reports _ _ = I;
    2.21  
    2.22 -fun block_reports depth (Paragraph lines) = fold (line_reports depth) lines
    2.23 -  | block_reports depth (List (_, body)) = fold (block_reports (depth + 1)) body;
    2.24 +val lines_pos = #1 o Antiquote.range o maps line_content;
    2.25 +
    2.26 +fun block_reports depth (Paragraph lines) =
    2.27 +      cons (lines_pos lines, Markup.markdown_paragraph) #>
    2.28 +      fold (line_reports depth) lines
    2.29 +  | block_reports depth (List ({kind, ...}, body)) =
    2.30 +      cons (lines_pos (maps block_lines body), Markup.markdown_list (print_kind kind)) #>
    2.31 +      fold (block_reports (depth + 1)) body;
    2.32  
    2.33  in
    2.34  
    2.35 -fun reports blocks = fold (block_reports 0) blocks [];
    2.36 +fun reports blocks =
    2.37 +  filter (Position.is_reported o #1) (fold (block_reports 0) blocks []);
    2.38  
    2.39  end;
    2.40  
     3.1 --- a/src/Tools/jEdit/src/rendering.scala	Thu Oct 15 15:06:03 2015 +0200
     3.2 +++ b/src/Tools/jEdit/src/rendering.scala	Thu Oct 15 16:12:38 2015 +0200
     3.3 @@ -155,7 +155,8 @@
     3.4      Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING,
     3.5        Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING,
     3.6        Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND,
     3.7 -      Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT)
     3.8 +      Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT,
     3.9 +      Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name)
    3.10  
    3.11    private val hyperlink_elements =
    3.12      Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION, Markup.URL)
    3.13 @@ -182,7 +183,8 @@
    3.14  
    3.15    private val tooltip_elements =
    3.16      Markup.Elements(Markup.LANGUAGE, Markup.TIMING, Markup.ENTITY, Markup.SORTING,
    3.17 -      Markup.TYPING, Markup.ML_TYPING, Markup.ML_BREAKPOINT, Markup.PATH, Markup.URL) ++
    3.18 +      Markup.TYPING, Markup.ML_TYPING, Markup.ML_BREAKPOINT, Markup.PATH, Markup.URL,
    3.19 +      Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name) ++
    3.20      Markup.Elements(tooltip_descriptions.keySet)
    3.21  
    3.22    private val gutter_elements =
    3.23 @@ -519,6 +521,7 @@
    3.24          {
    3.25            case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
    3.26              Some(Text.Info(r, (t1 + t2, info)))
    3.27 +
    3.28            case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
    3.29              val kind1 = Word.implode(Word.explode('_', kind))
    3.30              val txt1 =
    3.31 @@ -530,19 +533,24 @@
    3.32                  "\n" + t.message
    3.33                else ""
    3.34              Some(add(prev, r, (true, XML.Text(txt1 + txt2))))
    3.35 +
    3.36            case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) =>
    3.37              val file = jedit_file(name)
    3.38              val text =
    3.39                if (name == file) "file " + quote(file)
    3.40                else "path " + quote(name) + "\nfile " + quote(file)
    3.41              Some(add(prev, r, (true, XML.Text(text))))
    3.42 +
    3.43            case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) =>
    3.44              Some(add(prev, r, (true, XML.Text("URL " + quote(name)))))
    3.45 +
    3.46            case (prev, Text.Info(r, XML.Elem(Markup(name, _), body)))
    3.47            if name == Markup.SORTING || name == Markup.TYPING =>
    3.48              Some(add(prev, r, (true, pretty_typing("::", body))))
    3.49 +
    3.50            case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
    3.51              Some(add(prev, r, (false, pretty_typing("ML:", body))))
    3.52 +
    3.53            case (prev, Text.Info(r, Protocol.ML_Breakpoint(breakpoint))) =>
    3.54              val text =
    3.55                if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)"
    3.56 @@ -550,6 +558,12 @@
    3.57              Some(add(prev, r, (true, XML.Text(text))))
    3.58            case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) =>
    3.59              Some(add(prev, r, (true, XML.Text("language: " + language))))
    3.60 +
    3.61 +          case (prev, Text.Info(r, XML.Elem(Markup(Markup.MARKDOWN_PARAGRAPH, _), _))) =>
    3.62 +            Some(add(prev, r, (true, XML.Text("Markdown: paragraph"))))
    3.63 +          case (prev, Text.Info(r, XML.Elem(Markup.Markdown_List(kind), _))) =>
    3.64 +            Some(add(prev, r, (true, XML.Text("Markdown: " + kind))))
    3.65 +
    3.66            case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) =>
    3.67              Rendering.tooltip_descriptions.get(name).
    3.68                map(descr => add(prev, r, (true, XML.Text(descr))))