author  wenzelm 
Wed, 21 Dec 2016 21:18:37 +0100  
changeset 64648  5d7f741aaccb 
parent 64622  529bbb8977c7 
child 64649  d67c3094a0c2 
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 
{ 
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

15 
private val hyperlink_elements = 
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

16 
Markup.Elements(Markup.ENTITY, Markup.PATH, Markup.POSITION, Markup.URL) 
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

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

18 

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

19 
class VSCode_Rendering(snapshot: Document.Snapshot, options: Options, resources: Resources) 
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset

20 
extends Rendering(snapshot, options, resources) 
529bbb8977c7
more uniform rendering for Isabelle/jEdit and Isabelle/VSCode;
wenzelm
parents:
diff
changeset

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

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

23 

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

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

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

26 

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

27 

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

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

29 

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

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

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

32 
snapshot.cumulate[List[(String, Line.Range)]]( 
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

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

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

35 
case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) => 
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

36 
Some((resolve_file_url(name), Line.Range.zero) :: links) 
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

37 

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

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

39 
case (links, Text.Info(_, XML.Elem(Markup.Url(name), _))) => 
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

40 
Some(PIDE.editor.hyperlink_url(name) :: links) 
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

41 

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

42 
case (links, Text.Info(info_range, XML.Elem(Markup(Markup.ENTITY, props), _))) 
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

43 
if !props.exists( 
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

44 
{ case (Markup.KIND, Markup.ML_OPEN) => true 
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

45 
case (Markup.KIND, Markup.ML_STRUCTURE) => true 
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

46 
case _ => false }) => 
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

47 
val opt_link = PIDE.editor.hyperlink_def_position(true, snapshot, props) 
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

48 
opt_link.map(_ :: links) 
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

49 

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

50 
case (links, Text.Info(info_range, XML.Elem(Markup(Markup.POSITION, props), _))) => 
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

51 
val opt_link = PIDE.editor.hyperlink_position(true, snapshot, props) 
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

52 
opt_link.map(_ :: links) 
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

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

54 

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

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

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

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

58 
} 