author | paulson <lp15@cam.ac.uk> |
Wed, 24 Apr 2024 20:56:26 +0100 | |
changeset 80149 | 40a3fc07a587 |
parent 76765 | c654103e9c9d |
permissions | -rw-r--r-- |
66098 | 1 |
/* Title: Tools/VSCode/src/preview_panel.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 |
|
75393 | 15 |
class Preview_Panel(resources: VSCode_Resources) { |
65983 | 16 |
private val pending = Synchronized(Map.empty[JFile, Int]) |
17 |
||
18 |
def request(file: JFile, column: Int): Unit = |
|
19 |
pending.change(map => map + (file -> column)) |
|
65977
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
diff
changeset
|
20 |
|
75393 | 21 |
def flush(channel: Channel): Boolean = { |
75394 | 22 |
pending.change_result { map => |
65983 | 23 |
val map1 = |
73359 | 24 |
map.iterator.foldLeft(map) { |
25 |
case (m, (file, column)) => |
|
26 |
resources.get_model(file) match { |
|
27 |
case Some(model) => |
|
76765
c654103e9c9d
more robust Document.Pending_Edits: cover all nodes simulataneously, and thus support proper Snapshot.switch;
wenzelm
parents:
75979
diff
changeset
|
28 |
val snapshot = resources.snapshot(model) |
73359 | 29 |
if (snapshot.is_outdated) m |
30 |
else { |
|
75979 | 31 |
val context = |
32 |
Browser_Info.context(resources.sessions_structure, |
|
33 |
elements = Browser_Info.extra_elements) |
|
34 |
val document = context.preview_document(snapshot) |
|
73359 | 35 |
channel.write(LSP.Preview_Response(file, column, document.title, document.content)) |
36 |
m - file |
|
37 |
} |
|
38 |
case None => m - file |
|
39 |
} |
|
40 |
} |
|
65983 | 41 |
(map1.nonEmpty, map1) |
75394 | 42 |
} |
65977
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
diff
changeset
|
43 |
} |
c51b74be23b6
provide preview content on Scala side (similar to output);
wenzelm
parents:
diff
changeset
|
44 |
} |