|
1 /* Title: Tools/Graphview/src/graph_components.scala |
|
2 Author: Markus Kaiser, TU Muenchen |
|
3 |
|
4 Tooltip generation for graph components. |
|
5 */ |
|
6 |
|
7 package isabelle.graphview |
|
8 |
|
9 |
|
10 import isabelle._ |
|
11 import java.awt.FontMetrics |
|
12 |
|
13 |
|
14 object Tooltips { |
|
15 // taken (and modified slightly) from html_panel.scala |
|
16 private def make_HTML(term: XML.Body, fm: FontMetrics): String = { |
|
17 XML.string_of_body ( term.flatMap(div => |
|
18 Pretty.formatted(List(div), 76, Pretty.font_metric(fm)) |
|
19 .map( t=> |
|
20 HTML.spans(t, false)) |
|
21 ).head |
|
22 ) |
|
23 } |
|
24 |
|
25 def locale(key: String, model: Model, fm: FontMetrics): String = { |
|
26 val locale = model.complete.get_node(key) |
|
27 val parsed_name = key.split('.') |
|
28 |
|
29 if (!locale.isDefined) { |
|
30 """|<html> |
|
31 |<body style="margin: 3px"> |
|
32 |%s |
|
33 |</body> |
|
34 |""".stripMargin.format(parsed_name.reduceLeft("%s<br>%s".format(_,_))) |
|
35 } else { |
|
36 val Some(Locale(axioms, parameters)) = locale |
|
37 |
|
38 val parms = { |
|
39 if (parameters.size > 0) { |
|
40 """| |
|
41 |<p>Parameters:</p> |
|
42 |<ul> |
|
43 |%s |
|
44 |</ul> |
|
45 |""".stripMargin.format(parameters.map( |
|
46 y => "<li>%s :: %s</li>".format( |
|
47 y._1, |
|
48 make_HTML(y._2, fm)) |
|
49 ).reduceLeft(_+_)) |
|
50 } else "" |
|
51 } |
|
52 val axms = { |
|
53 if (axioms.size > 0) { |
|
54 """| |
|
55 |<p>Axioms:</p> |
|
56 |<ul> |
|
57 |%s |
|
58 |</ul> |
|
59 |""".stripMargin.format(axioms.map( |
|
60 y => "<li>%s</li>".format( |
|
61 make_HTML(y, fm)) |
|
62 ).reduceLeft(_+_)) |
|
63 } else "" |
|
64 } |
|
65 |
|
66 """|<html> |
|
67 |<style type="text/css"> |
|
68 |/* isabelle style */ |
|
69 |%s |
|
70 | |
|
71 |/* tooltip specific style */ |
|
72 | |
|
73 |body { margin: 10px; font-size: 12px; } |
|
74 |hr { margin: 12px 0 0 0; height: 2px; } |
|
75 |p { margin: 6px 0 2px 0; } |
|
76 |ul { margin: 0 0 0 4px; list-style-type: none; } |
|
77 |li { margin: 0 0 4px; } |
|
78 | |
|
79 |</style> |
|
80 |<body> |
|
81 |<center>%s</center> |
|
82 |<hr> |
|
83 |%s |
|
84 |%s |
|
85 |</body> |
|
86 |</html> |
|
87 |""".stripMargin.format(Parameters.tooltip_css, |
|
88 parsed_name.reduceLeft("%s<br>%s".format(_,_)), |
|
89 axms, |
|
90 parms).replace("'", "'") |
|
91 } |
|
92 } |
|
93 } |