38 |
38 |
39 def refresh(output: List[XML.Elem]): Unit = { |
39 def refresh(output: List[XML.Elem]): Unit = { |
40 val formatted = |
40 val formatted = |
41 Pretty.formatted(Pretty.separate(output), margin = margin, metric = Symbol.Metric) |
41 Pretty.formatted(Pretty.separate(output), margin = margin, metric = Symbol.Metric) |
42 |
42 |
43 if (formatted == current_formatted) return |
43 if (formatted != current_formatted) { |
|
44 current_output = output |
|
45 current_formatted = formatted |
44 |
46 |
45 current_output = output |
47 if (resources.html_output) { |
46 current_formatted = formatted |
48 val node_context = |
|
49 new Browser_Info.Node_Context { |
|
50 override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] = |
|
51 for { |
|
52 thy_file <- Position.Def_File.unapply(props) |
|
53 def_line <- Position.Def_Line.unapply(props) |
|
54 source <- resources.source_file(thy_file) |
|
55 uri = File.uri(Path.explode(source).absolute_file) |
|
56 } yield HTML.link(uri.toString + "#" + def_line, body) |
|
57 } |
|
58 val elements = Browser_Info.extra_elements.copy(entity = Markup.Elements.full) |
|
59 val html = node_context.make_html(elements, formatted) |
|
60 val message = output_json(HTML.source(html).toString, None) |
|
61 channel.write(message) |
|
62 } |
|
63 else { |
|
64 def convert_symbols(body: XML.Body): XML.Body = |
|
65 body.map { |
|
66 case XML.Elem(markup, body) => XML.Elem(markup, convert_symbols(body)) |
|
67 case XML.Text(content) => XML.Text(resources.output_text(content)) |
|
68 } |
47 |
69 |
48 if (resources.html_output) { |
70 val converted = convert_symbols(formatted) |
49 val node_context = |
71 |
50 new Browser_Info.Node_Context { |
72 val tree = Markup_Tree.from_XML(converted) |
51 override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] = |
73 val text = XML.content(converted) |
52 for { |
74 |
53 thy_file <- Position.Def_File.unapply(props) |
75 val document = Line.Document(text) |
54 def_line <- Position.Def_Line.unapply(props) |
76 val decorations = |
55 source <- resources.source_file(thy_file) |
77 tree.cumulate[Option[Markup]](Text.Range.full, None, Rendering.text_color_elements, |
56 uri = File.uri(Path.explode(source).absolute_file) |
78 { case (_, m) => Some(Some(m.info.markup)) } |
57 } yield HTML.link(uri.toString + "#" + def_line, body) |
79 ).flatMap(info => |
58 } |
80 info.info match { |
59 val elements = Browser_Info.extra_elements.copy(entity = Markup.Elements.full) |
81 case Some(markup) => |
60 val html = node_context.make_html(elements, formatted) |
82 val range = document.range(info.range) |
61 val message = output_json(HTML.source(html).toString, None) |
83 Some((range, "text_" + Rendering.get_text_color(markup).get.toString)) |
62 channel.write(message) |
84 case None => None |
63 } else { |
85 } |
64 def convert_symbols(body: XML.Body): XML.Body = { |
86 ).groupMap(_._2)(e => LSP.Decoration_Options(e._1, Nil)).toList |
65 body.map { |
87 |
66 case XML.Elem(markup, body) => XML.Elem(markup, convert_symbols(body)) |
88 channel.write(output_json(text, Some(LSP.Decoration(decorations)))) |
67 case XML.Text(content) => XML.Text(resources.output_text(content)) |
|
68 } |
|
69 } |
89 } |
70 |
|
71 val converted = convert_symbols(formatted) |
|
72 |
|
73 val tree = Markup_Tree.from_XML(converted) |
|
74 val text = XML.content(converted) |
|
75 |
|
76 val document = Line.Document(text) |
|
77 val decorations = |
|
78 tree.cumulate[Option[Markup]](Text.Range.full, None, Rendering.text_color_elements, |
|
79 { case (_, m) => Some(Some(m.info.markup)) } |
|
80 ).flatMap(info => |
|
81 info.info match { |
|
82 case Some(markup) => |
|
83 val range = document.range(info.range) |
|
84 Some((range, "text_" + Rendering.get_text_color(markup).get.toString)) |
|
85 case None => None |
|
86 } |
|
87 ).groupMap(_._2)(e => LSP.Decoration_Options(e._1, Nil)).toList |
|
88 |
|
89 channel.write(output_json(text, Some(LSP.Decoration(decorations)))) |
|
90 } |
90 } |
91 } |
91 } |
92 } |
92 } |