author | wenzelm |
Fri, 01 Apr 2022 17:06:10 +0200 | |
changeset 75393 | 87ebf5a50283 |
parent 75154 | 3b5aa38282bd |
child 75701 | 84990c95712d |
permissions | -rw-r--r-- |
65191
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
1 |
/* Title: Tools/VSCode/src/dynamic_output.scala |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
3 |
|
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
4 |
Dynamic output, depending on caret focus: messages, state etc. |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
5 |
*/ |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
6 |
|
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
7 |
package isabelle.vscode |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
8 |
|
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
9 |
|
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
10 |
import isabelle._ |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
11 |
|
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
12 |
|
75393 | 13 |
object Dynamic_Output { |
14 |
sealed case class State(do_update: Boolean = true, output: List[XML.Tree] = Nil) { |
|
65193 | 15 |
def handle_update( |
75393 | 16 |
resources: VSCode_Resources, |
17 |
channel: Channel, |
|
18 |
restriction: Option[Set[Command]] |
|
19 |
): State = { |
|
65193 | 20 |
val st1 = |
65976 | 21 |
resources.get_caret() match { |
65193 | 22 |
case None => copy(output = Nil) |
66086 | 23 |
case Some(caret) => |
24 |
val snapshot = caret.model.snapshot() |
|
65193 | 25 |
if (do_update && !snapshot.is_outdated) { |
66086 | 26 |
snapshot.current_command(caret.node_name, caret.offset) match { |
65193 | 27 |
case None => copy(output = Nil) |
28 |
case Some(command) => |
|
29 |
copy(output = |
|
71383 | 30 |
if (restriction.isEmpty || restriction.get.contains(command)) |
65195 | 31 |
Rendering.output_messages(snapshot.command_results(command)) |
65193 | 32 |
else output) |
33 |
} |
|
34 |
} |
|
35 |
else this |
|
36 |
} |
|
37 |
if (st1.output != output) { |
|
75154
3b5aa38282bd
proper Presentation.Entity_Context for hyperlinks (amending da1108a6d249);
wenzelm
parents:
75126
diff
changeset
|
38 |
val context = |
3b5aa38282bd
proper Presentation.Entity_Context for hyperlinks (amending da1108a6d249);
wenzelm
parents:
75126
diff
changeset
|
39 |
new Presentation.Entity_Context { |
3b5aa38282bd
proper Presentation.Entity_Context for hyperlinks (amending da1108a6d249);
wenzelm
parents:
75126
diff
changeset
|
40 |
override def make_ref(props: Properties.T, body: XML.Body): Option[XML.Elem] = |
3b5aa38282bd
proper Presentation.Entity_Context for hyperlinks (amending da1108a6d249);
wenzelm
parents:
75126
diff
changeset
|
41 |
for { |
3b5aa38282bd
proper Presentation.Entity_Context for hyperlinks (amending da1108a6d249);
wenzelm
parents:
75126
diff
changeset
|
42 |
thy_file <- Position.Def_File.unapply(props) |
3b5aa38282bd
proper Presentation.Entity_Context for hyperlinks (amending da1108a6d249);
wenzelm
parents:
75126
diff
changeset
|
43 |
def_line <- Position.Def_Line.unapply(props) |
3b5aa38282bd
proper Presentation.Entity_Context for hyperlinks (amending da1108a6d249);
wenzelm
parents:
75126
diff
changeset
|
44 |
source <- resources.source_file(thy_file) |
3b5aa38282bd
proper Presentation.Entity_Context for hyperlinks (amending da1108a6d249);
wenzelm
parents:
75126
diff
changeset
|
45 |
uri = Path.explode(source).absolute_file.toURI |
3b5aa38282bd
proper Presentation.Entity_Context for hyperlinks (amending da1108a6d249);
wenzelm
parents:
75126
diff
changeset
|
46 |
} yield HTML.link(uri.toString + "#" + def_line, body) |
3b5aa38282bd
proper Presentation.Entity_Context for hyperlinks (amending da1108a6d249);
wenzelm
parents:
75126
diff
changeset
|
47 |
} |
3b5aa38282bd
proper Presentation.Entity_Context for hyperlinks (amending da1108a6d249);
wenzelm
parents:
75126
diff
changeset
|
48 |
val elements = Presentation.elements2.copy(entity = Markup.Elements.full) |
3b5aa38282bd
proper Presentation.Entity_Context for hyperlinks (amending da1108a6d249);
wenzelm
parents:
75126
diff
changeset
|
49 |
val html = Presentation.make_html(context, elements, Pretty.separate(st1.output)) |
3b5aa38282bd
proper Presentation.Entity_Context for hyperlinks (amending da1108a6d249);
wenzelm
parents:
75126
diff
changeset
|
50 |
channel.write(LSP.Dynamic_Output(HTML.source(html).toString)) |
65193 | 51 |
} |
52 |
st1 |
|
53 |
} |
|
54 |
} |
|
65191
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
55 |
|
72761 | 56 |
def apply(server: Language_Server): Dynamic_Output = new Dynamic_Output(server) |
65191
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
57 |
} |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
58 |
|
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
59 |
|
75393 | 60 |
class Dynamic_Output private(server: Language_Server) { |
65191
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
61 |
private val state = Synchronized(Dynamic_Output.State()) |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
62 |
|
73340 | 63 |
private def handle_update(restriction: Option[Set[Command]]): Unit = |
64 |
state.change(_.handle_update(server.resources, server.channel, restriction)) |
|
65191
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
65 |
|
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
66 |
|
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
67 |
/* main */ |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
68 |
|
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
69 |
private val main = |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
70 |
Session.Consumer[Any](getClass.getName) { |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
71 |
case changed: Session.Commands_Changed => |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
72 |
handle_update(if (changed.assignment) None else Some(changed.commands)) |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
73 |
|
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
74 |
case Session.Caret_Focus => |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
75 |
handle_update(None) |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
76 |
} |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
77 |
|
75393 | 78 |
def init(): Unit = { |
65191
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
79 |
server.session.commands_changed += main |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
80 |
server.session.caret_focus += main |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
81 |
handle_update(None) |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
82 |
} |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
83 |
|
75393 | 84 |
def exit(): Unit = { |
65191
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
85 |
server.session.commands_changed -= main |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
86 |
server.session.caret_focus -= main |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
87 |
} |
4c9c83311cad
dynamic output, depending on caret focus (see also Tools/jEdit/src/output_dockable.scala);
wenzelm
parents:
diff
changeset
|
88 |
} |