author | wenzelm |
Thu, 08 Jun 2017 14:08:07 +0200 | |
changeset 66040 | f826ba18fe08 |
parent 66000 | 58aa6749ff36 |
permissions | -rw-r--r-- |
65983 | 1 |
/* Title: Tools/VSCode/src/preview.scala |
65977
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
diff
changeset
|
3 |
|
65983 | 4 |
HTML document preview. |
65977
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
diff
changeset
|
5 |
*/ |
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
diff
changeset
|
6 |
|
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
diff
changeset
|
7 |
package isabelle.vscode |
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
diff
changeset
|
8 |
|
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
diff
changeset
|
9 |
|
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
diff
changeset
|
10 |
import isabelle._ |
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
diff
changeset
|
11 |
|
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
diff
changeset
|
12 |
import java.io.{File => JFile} |
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
diff
changeset
|
13 |
|
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
diff
changeset
|
14 |
|
65983 | 15 |
class Preview(resources: VSCode_Resources) |
65977
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
diff
changeset
|
16 |
{ |
65983 | 17 |
private val pending = Synchronized(Map.empty[JFile, Int]) |
18 |
||
19 |
def request(file: JFile, column: Int): Unit = |
|
20 |
pending.change(map => map + (file -> column)) |
|
65977
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
diff
changeset
|
21 |
|
65983 | 22 |
def flush(channel: Channel): Boolean = |
65977
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
diff
changeset
|
23 |
{ |
65983 | 24 |
pending.change_result(map => |
25 |
{ |
|
26 |
val map1 = |
|
27 |
(map /: map.iterator)({ case (m, (file, column)) => |
|
28 |
resources.get_model(file) match { |
|
29 |
case Some(model) => |
|
30 |
val snapshot = model.snapshot() |
|
31 |
if (snapshot.is_outdated) m |
|
32 |
else { |
|
33 |
val (label, content) = make_preview(model, snapshot) |
|
34 |
channel.write(Protocol.Preview_Response(file, column, label, content)) |
|
35 |
m - file |
|
36 |
} |
|
37 |
case None => m - file |
|
38 |
} |
|
39 |
}) |
|
40 |
(map1.nonEmpty, map1) |
|
41 |
}) |
|
65977
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
diff
changeset
|
42 |
} |
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
diff
changeset
|
43 |
|
65983 | 44 |
def make_preview(model: Document_Model, snapshot: Document.Snapshot): (String, String) = |
65977
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
diff
changeset
|
45 |
{ |
65983 | 46 |
val label = "Preview " + quote(model.node_name.toString) |
47 |
val content = |
|
66000 | 48 |
HTML.output_document( |
49 |
List(HTML.style(HTML.fonts_css()), HTML.style_file(Url.print_file(HTML.isabelle_css.file))), |
|
65983 | 50 |
List( |
65995 | 51 |
HTML.chapter("Theory " + quote(model.node_name.theory_base_name)), |
66040 | 52 |
HTML.source(Present.theory_document(snapshot))), |
66000 | 53 |
css = "") |
65983 | 54 |
(label, content) |
65977
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
diff
changeset
|
55 |
} |
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
diff
changeset
|
56 |
} |