author  wenzelm 
Wed, 21 Dec 2016 22:27:38 +0100  
changeset 64649  d67c3094a0c2 
parent 64648  5d7f741aaccb 
child 64651  ea5620f7b0d8 
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 

64649  19 
class VSCode_Rendering( 
20 
val model: Document_Model, 

21 
snapshot: Document.Snapshot, 

22 
options: Options, 

23 
resources: Resources) 

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

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

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

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

27 

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

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

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

30 

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 
/* hyperlinks */ 
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

33 

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

35 
{ 
64649  36 
snapshot.cumulate[List[Line.Range_Node]]( 
64648
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

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

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

39 
case (links, Text.Info(_, XML.Elem(Markup.Path(name), _))) => 
64649  40 
Some(Line.Range_Node(Line.Range.zero, resolve_file_url(name)) :: links) 
64648
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 
/* FIXME 
5d7f741aaccb
basic support for hyperlinks / Goto Definition Request;
wenzelm
parents:
64622
diff
changeset

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

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

45 

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

46 
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

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

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

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

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

51 
val opt_link = PIDE.editor.hyperlink_def_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 
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

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

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

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

58 

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

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

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

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

62 
} 