# HG changeset patch # User wenzelm # Date 1444918358 -7200 # Node ID 239a04ec2d4ce5c717847c1a10fe3b802c5592c1 # Parent 4f31f79cf2d1ba80cc21544c81a02817596249d3 more markup; diff -r 4f31f79cf2d1 -r 239a04ec2d4c src/Pure/General/antiquote.ML --- a/src/Pure/General/antiquote.ML Thu Oct 15 15:06:03 2015 +0200 +++ b/src/Pure/General/antiquote.ML Thu Oct 15 16:12:38 2015 +0200 @@ -9,6 +9,7 @@ type antiq = Symbol_Pos.T list * {start: Position.T, stop: Position.T, range: Position.range} datatype 'a antiquote = Text of 'a | Antiq of antiq type text_antiquote = Symbol_Pos.T list antiquote + val range: text_antiquote list -> Position.range val split_lines: text_antiquote list -> text_antiquote list list val antiq_reports: antiq -> Position.report list val antiquote_reports: ('a -> Position.report_text list) -> @@ -28,6 +29,13 @@ type text_antiquote = Symbol_Pos.T list antiquote; +fun antiquote_range (Text ss) = Symbol_Pos.range ss + | antiquote_range (Antiq (_, {range, ...})) = range; + +fun range ants = + if null ants then Position.no_range + else Position.range (#1 (antiquote_range (hd ants))) (#2 (antiquote_range (List.last ants))); + (* split lines *) diff -r 4f31f79cf2d1 -r 239a04ec2d4c src/Pure/Thy/markdown.ML --- a/src/Pure/Thy/markdown.ML Thu Oct 15 15:06:03 2015 +0200 +++ b/src/Pure/Thy/markdown.ML Thu Oct 15 16:12:38 2015 +0200 @@ -104,6 +104,10 @@ datatype block = Paragraph of line list | List of marker * block list; +fun block_lines (Paragraph lines) = lines + | block_lines (List (_, blocks)) = maps block_lines blocks; + + fun add_span (opt_marker, body) document = (case (opt_marker, document) of (SOME marker, (list as List (list_marker, list_body)) :: rest) => @@ -154,15 +158,22 @@ local fun line_reports depth (Line {marker = SOME (_, pos), ...}) = - Position.is_reported pos ? cons (pos, Markup.markdown_item depth) + cons (pos, Markup.markdown_item depth) | line_reports _ _ = I; -fun block_reports depth (Paragraph lines) = fold (line_reports depth) lines - | block_reports depth (List (_, body)) = fold (block_reports (depth + 1)) body; +val lines_pos = #1 o Antiquote.range o maps line_content; + +fun block_reports depth (Paragraph lines) = + cons (lines_pos lines, Markup.markdown_paragraph) #> + fold (line_reports depth) lines + | block_reports depth (List ({kind, ...}, body)) = + cons (lines_pos (maps block_lines body), Markup.markdown_list (print_kind kind)) #> + fold (block_reports (depth + 1)) body; in -fun reports blocks = fold (block_reports 0) blocks []; +fun reports blocks = + filter (Position.is_reported o #1) (fold (block_reports 0) blocks []); end; diff -r 4f31f79cf2d1 -r 239a04ec2d4c src/Tools/jEdit/src/rendering.scala --- a/src/Tools/jEdit/src/rendering.scala Thu Oct 15 15:06:03 2015 +0200 +++ b/src/Tools/jEdit/src/rendering.scala Thu Oct 15 16:12:38 2015 +0200 @@ -155,7 +155,8 @@ Markup.Elements(Markup.EXPRESSION, Markup.CITATION, Markup.LANGUAGE, Markup.ML_TYPING, Markup.TOKEN_RANGE, Markup.ENTITY, Markup.PATH, Markup.URL, Markup.SORTING, Markup.TYPING, Markup.FREE, Markup.SKOLEM, Markup.BOUND, - Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT) + Markup.VAR, Markup.TFREE, Markup.TVAR, Markup.ML_BREAKPOINT, + Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name) private val hyperlink_elements = Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.CITATION, Markup.URL) @@ -182,7 +183,8 @@ 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.URL) ++ + Markup.TYPING, Markup.ML_TYPING, Markup.ML_BREAKPOINT, Markup.PATH, Markup.URL, + Markup.MARKDOWN_PARAGRAPH, Markup.Markdown_List.name) ++ Markup.Elements(tooltip_descriptions.keySet) private val gutter_elements = @@ -519,6 +521,7 @@ { case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) => Some(Text.Info(r, (t1 + t2, info))) + case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) => val kind1 = Word.implode(Word.explode('_', kind)) val txt1 = @@ -530,19 +533,24 @@ "\n" + t.message else "" Some(add(prev, r, (true, XML.Text(txt1 + txt2)))) + case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _))) => val file = jedit_file(name) val text = if (name == file) "file " + quote(file) else "path " + quote(name) + "\nfile " + quote(file) Some(add(prev, r, (true, XML.Text(text)))) + case (prev, Text.Info(r, XML.Elem(Markup.Url(name), _))) => Some(add(prev, r, (true, XML.Text("URL " + quote(name))))) + case (prev, Text.Info(r, XML.Elem(Markup(name, _), body))) if name == Markup.SORTING || name == Markup.TYPING => Some(add(prev, r, (true, pretty_typing("::", body)))) + case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) => Some(add(prev, r, (false, pretty_typing("ML:", body)))) + case (prev, Text.Info(r, Protocol.ML_Breakpoint(breakpoint))) => val text = if (Debugger.breakpoint_state(breakpoint)) "breakpoint (enabled)" @@ -550,6 +558,12 @@ Some(add(prev, r, (true, XML.Text(text)))) case (prev, Text.Info(r, XML.Elem(Markup.Language(language, _, _, _), _))) => Some(add(prev, r, (true, XML.Text("language: " + language)))) + + 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), _))) => + Some(add(prev, r, (true, XML.Text("Markdown: " + kind)))) + case (prev, Text.Info(r, XML.Elem(Markup(name, _), _))) => Rendering.tooltip_descriptions.get(name). map(descr => add(prev, r, (true, XML.Text(descr))))