时间戳

首页 > 解决方案 > 使用 VS Code 扩展时出错

visual-studio-code - 使用 VS Code 扩展时出错

问题描述

我尝试使用 Isabelle 2019 的 VS Code 扩展。当我尝试打开 Isabelle 输出时，出现异常

线程“event_timer”中的异常java.util.NoSuchElementException：找不到键：
scala.collection.MapLike.default（MapLike.scala：231）的IsabelleDejaVuSans.ttf在
scala.collection.MapLike.default$（MapLike.scala：230）
在 scala.collection.AbstractMap.default(Map.scala:59)
在 scala.collection.MapLike.apply(MapLike.scala:140)
在 scala.collection.MapLike.apply$(MapLike.scala:139)
在 scala.collection .AbstractMap.apply(Map.scala:59)
在 isabelle.HTML$.font_face$1(html.scala:366)
在 isabelle.HTML$.$anonfun$fonts_css$1(html.scala:371)
在 scala.collection.immutable .List.map(List.scala:282)
在 isabelle.HTML$.fonts_css(html.scala:371)
在 isabelle.Present$.output_document$1(present.scala:120)
在 isabelle.Present$.preview(present.scala:138)
在 isabelle.vscode.Preview_Panel.$anonfun$flush$2(preview_panel.scala:33)
在 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( Ite​​rator.scala :937)
at scala.collection.Iterator.foreach$(Iterator.scala:937)
at scala.collection.AbstractIterator.foreach(Ite​​rator.scala:1425)
at scala.collection.TraversableOnce.foldLeft(TraversableOnce.scala:156)
at scala.collection.TraversableOnce.foldLeft$(TraversableOnce.scala:154)
在 scala.collection.AbstractIterator.foldLeft(Iterator.scala:1425)
在 scala.collection.TraversableOnce.$div$colon(TraversableOnce.scala:150)
在 scala.collection.TraversableOnce.$div$colon$(TraversableOnce.scala: 150)
在 scala.collection.AbstractIterator.$div$colon(Iterator.scala:1425)
在 isabelle.vscode.Preview_Panel.$anonfun$flush$1(preview_panel.scala:27​​)
在 isabelle.Synchronized.change_result(synchronized.scala: 73)
在 isabelle.vscode.Preview_Panel.flush(preview_panel.scala:24)
在 isabelle.vscode.Server.$anonfun$delay_preview$2(server.scala:210)
在 isabelle.Standard_Thread$Delay.run(standard_thread.scala:64 )
在 isabelle.Standard_Thread$Delay.$anonfun$invoke$1(standard_thread.scala:77)
在 isabelle.Event_Timer$$anon$1.run(event_timer.scala:27​​)
在 java.base/java.util.TimerThread.mainLoop(Timer .java:556)
在 java.base/java.util.TimerThread.run(Timer.java:506)

如果我然后做任何其他事情（例如在代码窗口中输入），每次都会引发另一个异常

[错误 - 晚上 9:01:48] java.lang.IllegalStateException：计时器已取消。

我怎样才能摆脱这两个错误？

我在这里发现了相同或类似的问题，他们建议运行

$ isabelle scala
scala> import isabelle._
scala> Isabelle_Fonts.fonts(hidden = true)

这导致

res0: List[isabelle.Isabelle_Fonts.Entry] = List(Entry("/home/daniel/opt/isabelle/contrib/isabelle_fonts-20190409/ttf-hinted/IsabelleDejaVuSans.ttf",false), Entry("/home/daniel /opt/isabelle/contrib/isabelle_fonts-20190409/ttf-hinted/IsabelleDejaVuSans-Bold.ttf",false), 条目("/home/daniel/opt/isabelle/contrib/isabelle_fonts-20190409/ttf-hinted/IsabelleDejaVuSans-Oblique .ttf",false), Entry("/home/daniel/opt/isabelle/contrib/isabelle_fonts-20190409/ttf-hinted/IsabelleDejaVuSans-BoldOblique.ttf",false), Entry("/home/daniel/opt/isabelle /contrib/isabelle_fonts-20190409/ttf-hinted/IsabelleDejaVuSansMono.ttf",false), 条目("/home/daniel/opt/isabelle/contrib/isabelle_fonts-20190409/ttf-hinted/IsabelleDejaVuSansMono-Bold.ttf",false) , Entry("/home/daniel/opt/isabelle/con...

标签： visual-studio-codeisabelle

解决方案

简单的答案：Isabelle2019 不支持 VSCode --- 该平台移动得太快并假设快速移动。

在 Isabelle2020（2020 年 4 月）中，它应该会再次起作用。此版本的近似值可在此处获得：https ://sketis.net/2020/release-process-for-isabelle2020

另请参阅https://marketplace.visualstudio.com/items?itemName=makarius.Isabelle2020

推荐阅读