|
1 /* Title: Tools/VSCode/src/preview.scala |
|
2 Author: Makarius |
|
3 |
|
4 HTML document preview. |
|
5 */ |
|
6 |
|
7 package isabelle.vscode |
|
8 |
|
9 |
|
10 import isabelle._ |
|
11 |
|
12 import java.io.{File => JFile} |
|
13 |
|
14 |
|
15 class Preview(resources: VSCode_Resources) |
|
16 { |
|
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)) |
|
21 |
|
22 def flush(channel: Channel): Boolean = |
|
23 { |
|
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 }) |
|
42 } |
|
43 |
|
44 def make_preview(model: Document_Model, snapshot: Document.Snapshot): (String, String) = |
|
45 { |
|
46 val label = "Preview " + quote(model.node_name.toString) |
|
47 val content = |
|
48 HTML.output_document(head = Nil, css = "", body = |
|
49 List( |
|
50 HTML.chapter(label), |
|
51 HTML.itemize( |
|
52 snapshot.node.commands.toList.flatMap( |
|
53 command => |
|
54 if (command.span.name == "") None |
|
55 else Some(HTML.text(command.span.name)))))) |
|
56 (label, content) |
|
57 } |
|
58 } |