Email Gateway (Aug 22 2022 at 20:36): Email Gateway (Aug 22 2022 at 20:36):From: Kevin Kappelmann <kevin.kappelmann@tum.de>
I wanted to use Isabelle2019 with VSCode. However, I cannot open the
state panel as the following error is thrown:
*** Consumer thread failure: "Session.dispatcher"
*** Consumer failed: "isabelle.vscode.State_Panel"
*** java.util.NoSuchElementException: key not found: IsabelleDejaVuSans.tt
I did install the font on my system (Ubuntu 18.04). In particular, I can
use it in VSCode. Anyone any ideas or similar experiences?
For people using Zulip, here is the corresponding discussion:
https://isabelle.zulipchat.com/#narrow/stream/202961-general/topic/VS.20Code
(screenshot appended for non-zulip users).
Best wishes,
Kevin.
zulip_vs_code.png
Email Gateway (Aug 22 2022 at 20:36):From: Makarius <makarius@sketis.net>
On 20/09/2019 11:28, Kevin Kappelmann wrote:
I wanted to use Isabelle2019 with VSCode. However, I cannot open the
state panel as the following error is thrown:*** Consumer thread failure: "Session.dispatcher"
*** Consumer failed: "isabelle.vscode.State_Panel"
*** java.util.NoSuchElementException: key not found: IsabelleDejaVuSans.ttI did install the font on my system (Ubuntu 18.04). In particular, I can
use it in VSCode. Anyone any ideas or similar experiences?
Just a guess from a distance:
apt-get install -y libfontconfig1
See also https://hub.docker.com/r/makarius/isabelle for Linux
requirements formalized via Docker.
Note that one thing is the VSCode editor front-end, another thing the
Isabelle/Scala backend. A Java exception means that the backend cannot
open the font, but that is configured automatically via Isabelle system
settings.
For people using Zulip, here is the corresponding discussion:
https://isabelle.zulipchat.com/#narrow/stream/202961-general/topic/VS.20Code
(screenshot appended for non-zulip users).
A discussion over many information exchange platforms is difficult. I
don't have the time to follow yet another cool new thing.
Makarius
Email Gateway (Aug 22 2022 at 20:36):From: Kevin Kappelmann <kevin.kappelmann@tum.de>
Thanks for the hint, but sadly, libfontconfig1 is already installed on
my machine. I started debugging the extension in VSCode. Here is the
stack trace I get when trying to open the preview panel:
[Error - 15:27:42] java.util.NoSuchElementException: key not found:
IsabelleDejaVuSans.ttf
Exception in thread "event_timer" java.util.NoSuchElementException: key
not found: IsabelleDejaVuSans.ttf
at scala.collection.MapLike.default(MapLike.scala:231)
at scala.collection.MapLike.default$(MapLike.scala:230)
at scala.collection.AbstractMap.default(Map.scala:59)
at scala.collection.MapLike.apply(MapLike.scala:140)
at scala.collection.MapLike.apply$(MapLike.scala:139)
at scala.collection.AbstractMap.apply(Map.scala:59)
at isabelle.HTML$.font_face$1(html.scala:366)
at isabelle.HTML$.$anonfun$fonts_css$1(html.scala:371)
at scala.collection.immutable.List.map(List.scala:282)
at isabelle.HTML$.fonts_css(html.scala:371)
at isabelle.Present$.output_document$1(present.scala:120)
at isabelle.Present$.preview(present.scala:138)
at isabelle.vscode.Preview_Panel.$anonfun$flush$2(preview_panel.scala:33)
at
scala.collection.TraversableOnce.$anonfun$foldLeft$1(TraversableOnce.scala:156)
at
scala.collection.TraversableOnce.$anonfun$foldLeft$1$adapted(TraversableOnce.scala:156)
at scala.collection.Iterator.foreach(Iterator.scala:937)
at scala.collection.Iterator.foreach$(Iterator.scala:937)
at scala.collection.AbstractIterator.foreach(Iterator.scala:1425)
at scala.collection.TraversableOnce.foldLeft(TraversableOnce.scala:156)
at scala.collection.TraversableOnce.foldLeft$(TraversableOnce.scala:154)
at scala.collection.AbstractIterator.foldLeft(Iterator.scala:1425)
at scala.collection.TraversableOnce.$div$colon(TraversableOnce.scala:150)
at scala.collection.TraversableOnce.$div$colon$(TraversableOnce.scala:150)
at scala.collection.AbstractIterator.$div$colon(Iterator.scala:1425)
at isabelle.vscode.Preview_Panel.$anonfun$flush$1(preview_panel.scala:27)
at isabelle.Synchronized.change_result(synchronized.scala:73)
at isabelle.vscode.Preview_Panel.flush(preview_panel.scala:24)
at isabelle.vscode.Server.$anonfun$delay_preview$2(server.scala:210)
at isabelle.Standard_Thread$Delay.run(standard_thread.scala:64)
at
isabelle.Standard_Thread$Delay.$anonfun$invoke$1(standard_thread.scala:77)
at isabelle.Event_Timer$$anon$1.run(event_timer.scala:27)
at java.base/java.util.TimerThread.mainLoop(Timer.java:556)
at java.base/java.util.TimerThread.run(Timer.java:506)
What source is isabelle.HTML$.font_face using to load fonts? Is it
looking in a specific folder or asking the system via some API for the
fonts?
Email Gateway (Aug 22 2022 at 20:36):From: Makarius <makarius@sketis.net>
The relevant Isabelle/Scala source is here:
https://isabelle.in.tum.de/repos/isabelle/file/Isabelle2019/src/Pure/Thy/html.scala#l359
You can try to core operation like this:
$ isabelle scala
scala> import isabelle._
scala> Isabelle_Fonts.fonts(hidden = true)
See also
https://isabelle.in.tum.de/repos/isabelle/file/Isabelle2019/src/Pure/System/isabelle_fonts.scala#l57
Makarius
Email Gateway (Aug 22 2022 at 20:36):From: Makarius <makarius@sketis.net>
Actually, there is something wrong in Isabelle/VSCode of Isabelle2019: I
get a similar exception trace.
Since this thread originated on Zulip Chat, I've somehow fallen into
"chat mode" on this mailing list, too, and thus produced quick answers
instead of good ones. I will now take time to figure out what the
situation really is ...
Makarius
Email Gateway (Aug 22 2022 at 20:36):From: Makarius <makarius@sketis.net>
See now the following change (for the next release after Isabelle2019):
https://isabelle.in.tum.de/repos/isabelle/rev/342b0a1fc86d
changeset: 70743:342b0a1fc86d
tag: tip
user: wenzelm
date: Sun Sep 22 19:04:11 2019 +0200
summary: proper file name instead of font name (amending dc9a39c3f75d);
This does not help much: VSCode has changed too much recently -- I get a
lot of JavaScript/TypeScript exceptions when starting up the Isabelle
extension. (When I tried it for the Isabelle2019 release, the situation
was not as bad.)
Due to the highly dynamic nature of VSCode such total failures of
existence are to be expected: When I published Isabelle/VSCode for the
first time with Isabelle2017 (October 2017), it was already clear that a
proper release would have to bundle a particular version of VSCode, like
Isabelle already bundles Java, Scala, jEdit and many other things. This
would annoy anybody who thinks that "latest" means "best" version, but
it is inevitable for a stable application.
Makarius
Email Gateway (Aug 22 2022 at 20:37):From: Kevin Kappelmann <kevin.kappelmann@tum.de>
Thanks for the patch.
Email Gateway (Aug 22 2022 at 20:37):From: Kevin Kappelmann <kevin.kappelmann@tum.de>
(Pressed sent by accident at previous e-mail, sorry)
Thanks for the patch.
The reason the state panel will not open now is that previewHtml was
deprecated in November 2019 and removed earlier this year:
https://github.com/microsoft/vscode/issues/62630
The fix is to use the Webview API instead:
https://code.visualstudio.com/api/extension-guides/webview
I think this sadly cannot be done by just replacing one function call
since it seems that the current extension was using content providers
for TextDocuments, which I think cannot be used for Webviews.
I think making the Webview API work with the extension would be quite
beneficial since we can then add more visual/interactive plugins to
Isabelle, e.g. diagrams for category theory.
Kevin.
Email Gateway (Aug 22 2022 at 20:39):From: Makarius <makarius@sketis.net>
On 23/09/2019 17:37, Kevin Kappelmann wrote:
The reason the state panel will not open now is that previewHtml was
deprecated in November 2019 and removed earlier this year:
https://github.com/microsoft/vscode/issues/62630
The fix is to use the Webview API instead:
https://code.visualstudio.com/api/extension-guides/webview
I think this sadly cannot be done by just replacing one function call
since it seems that the current extension was using content providers
for TextDocuments, which I think cannot be used for Webviews.
https://code.visualstudio.com/api/extension-guides/webview is
indeed the missing link that I was looking for. I have somehow lost
track of the many ongoing changes in VSCode, but this looks like a
long-awaited reform for custom HTML content.
I think making the Webview API work with the extension would be quite
beneficial since we can then add more visual/interactive plugins to
Isabelle, e.g. diagrams for category theory.
Yes, I have recently started to look at high-end graph editors like
https://github.com/jgraph/mxgraph
The HTML container of VSCode might help to make this accessible in the
Isabelle Prover IDE, but Isabelle/VSCode is a very poor PIDE front-end
at the moment.
It might be easier to upgrade the Java/Swing GUI environment of
Isabelle/jEdit by Java Chromium Embedded
https://bitbucket.org/chromiumembedded/java-cef and thus have the
existing editor augmented by browser technology.
Makarius
Last updated: Nov 21 2024 at 12:39 UTC