author  wenzelm 
Thu, 29 Dec 2016 22:10:29 +0100  
changeset 64704  08c2d80428ff 
parent 64702  d95b9117cb5b 
child 64706  3ebf9f8299df 
permissions  rwrr 
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset

1 
/* Title: Tools/VSCode/src/vscode_rendering.scala 
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset

2 
Author: Makarius 
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset

3 

529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset

4 
Isabelle/VSCodespecific implementation of quasiabstract rendering and 
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset

5 
markup interpretation. 
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset

6 
*/ 
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset

7 

529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset

8 
package isabelle.vscode 
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset

9 

529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset

10 

529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset

11 
import isabelle._ 
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset

12 

64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

13 
object VSCode_Rendering 
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

14 
{ 
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

15 
/* diagnostic messages */ 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

16 

b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

17 
private val message_severity = 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

18 
Map( 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

19 
Markup.WRITELN > Protocol.DiagnosticSeverity.Hint, 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

20 
Markup.INFORMATION > Protocol.DiagnosticSeverity.Information, 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

21 
Markup.WARNING > Protocol.DiagnosticSeverity.Warning, 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

22 
Markup.LEGACY > Protocol.DiagnosticSeverity.Warning, 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

23 
Markup.ERROR > Protocol.DiagnosticSeverity.Error, 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

24 
Markup.BAD > Protocol.DiagnosticSeverity.Error) 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

25 

b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

26 

b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

27 
/* markup elements */ 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

28 

b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

29 
private val diagnostics_elements = 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

30 
Markup.Elements(Markup.WRITELN, Markup.INFORMATION, Markup.WARNING, Markup.LEGACY, Markup.ERROR, 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

31 
Markup.BAD) 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

32 

64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

33 
private val hyperlink_elements = 
64652  34 
Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION) 
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

35 
} 
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset

36 

64649  37 
class VSCode_Rendering( 
38 
val model: Document_Model, 

39 
snapshot: Document.Snapshot, 

64702  40 
resources: VSCode_Resources) 
64704  41 
extends Rendering(snapshot, resources.options, resources) 
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset

42 
{ 
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

43 
/* diagnostics */ 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

44 

b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

45 
def diagnostics: List[Text.Info[Command.Results]] = 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

46 
snapshot.cumulate[Command.Results]( 
64688
d8f194556c70
precise full_range and thus proper try_restrict in Snapshot.cumulate;
wenzelm
parents:
64683
diff
changeset

47 
model.doc.full_range, Command.Results.empty, VSCode_Rendering.diagnostics_elements, _ => 
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

48 
{ 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

49 
case (res, Text.Info(_, msg @ XML.Elem(Markup(_, Markup.Serial(i)), body))) 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

50 
if body.nonEmpty => Some(res + (i > msg)) 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

51 

b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

52 
case _ => None 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

53 
}) 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

54 

b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

55 
val diagnostics_margin = options.int("vscode_diagnostics_margin") 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

56 

b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

57 
def diagnostics_output(results: List[Text.Info[Command.Results]]): List[Protocol.Diagnostic] = 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

58 
{ 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

59 
(for { 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

60 
Text.Info(text_range, res) < results.iterator 
64683
c0c09b6dfbe0
clarified signature: maintan Text.Length within Line.Document;
wenzelm
parents:
64679
diff
changeset

61 
range = model.doc.range(text_range) 
64679
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

62 
(_, XML.Elem(Markup(name, _), body)) < res.iterator 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

63 
} yield { 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

64 
val message = Pretty.string_of(body, margin = diagnostics_margin) 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

65 
val severity = VSCode_Rendering.message_severity.get(name) 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

66 
Protocol.Diagnostic(range, message, severity = severity) 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

67 
}).toList 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

68 
} 
b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

69 

b2bf280b7e13
more uniform treatment of input/output wrt. client;
wenzelm
parents:
64668
diff
changeset

70 

64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset

71 
/* tooltips */ 
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset

72 

529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset

73 
def tooltip_margin: Int = options.int("vscode_tooltip_margin") 
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset

74 
def timing_threshold: Double = options.real("vscode_timing_threshold") 
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

75 

5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

76 

5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

77 
/* hyperlinks */ 
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

78 

64667  79 
def hyperlink_source_file(source_name: String, line1: Int, range: Symbol.Range) 
80 
: Option[Line.Node_Range] = 

81 
{ 

82 
for (name < resources.source_file(source_name)) 

83 
yield { 

84 
val opt_text = 

85 
try { Some(File.read(Path.explode(name))) } // FIXME content from resources/models 

86 
catch { case ERROR(_) => None } 

64668  87 
Line.Node_Range(File.platform_url(name), 
64667  88 
opt_text match { 
89 
case Some(text) if range.start > 0 => 

90 
val chunk = Symbol.Text_Chunk(text) 

64683
c0c09b6dfbe0
clarified signature: maintan Text.Length within Line.Document;
wenzelm
parents:
64679
diff
changeset

91 
val doc = Line.Document(text, model.doc.text_length) 
c0c09b6dfbe0
clarified signature: maintan Text.Length within Line.Document;
wenzelm
parents:
64679
diff
changeset

92 
doc.range(chunk.decode(range)) 
64667  93 
case _ => 
94 
Line.Range(Line.Position((line1  1) max 0)) 

95 
}) 

96 
} 

97 
} 

98 

99 
def hyperlink_command(id: Document_ID.Generic, range: Symbol.Range): Option[Line.Node_Range] = 

100 
{ 

101 
if (snapshot.is_outdated) None 

102 
else 

103 
for { 

104 
start < snapshot.find_command_position(id, range.start) 

105 
stop < snapshot.find_command_position(id, range.stop) 

106 
} yield Line.Node_Range(start.name, Line.Range(start.pos, stop.pos)) 

107 
} 

108 

109 
def hyperlink_position(pos: Position.T): Option[Line.Node_Range] = 

110 
pos match { 

111 
case Position.Item_File(name, line, range) => hyperlink_source_file(name, line, range) 

112 
case Position.Item_Id(id, range) => hyperlink_command(id, range) 

113 
case _ => None 

114 
} 

115 

116 
def hyperlink_def_position(pos: Position.T): Option[Line.Node_Range] = 

117 
pos match { 

118 
case Position.Item_Def_File(name, line, range) => hyperlink_source_file(name, line, range) 

119 
case Position.Item_Def_Id(id, range) => hyperlink_command(id, range) 

120 
case _ => None 

121 
} 

122 

64651  123 
def hyperlinks(range: Text.Range): List[Line.Node_Range] = 
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

124 
{ 
64651  125 
snapshot.cumulate[List[Line.Node_Range]]( 
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

126 
range, Nil, VSCode_Rendering.hyperlink_elements, _ => 
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

127 
{ 
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

128 
case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) => 
64654  129 
val file = resources.append_file_url(snapshot.node_name.master_dir, name) 
130 
Some(Line.Node_Range(file) :: links) 

64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

131 

64667  132 
case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) => 
133 
hyperlink_def_position(props).map(_ :: links) 

134 

135 
case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) => 

136 
hyperlink_position(props).map(_ :: links) 

64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

137 

5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

138 
case _ => None 
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

139 
}) match { case Text.Info(_, links) :: _ => links.reverse case _ => Nil } 
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

140 
} 
64622
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset

141 
} 