search

m-fleury / isabelle-emacs

Clone of isabelle, with LSP extensions in seperate branches
Other
24 stars 5 forks source link

Try emacs's xwidget to output goal #77

Open m-fleury opened 1 year ago

m-fleury commented 1 year ago

xwidget are optional and use webkit to print the goal -- outside of the main thread! So this should improve performance. Remark that the goal is already given as an HTML data anyway.

Currently, the HTML is communicated to another emacs thread, parsed, the HTML is stripped, the syntax highlighting is split and finally the text and the syntax highlighting are communicated back to be applied.

There are a few open questions like how the Sledgemmer/try0 output is handled, but this is worth a try.

m-fleury commented 1 year ago

How to open the buffer:


(defun test ()
  (let ((id (make-xwidget 'webkit "test" 200 200)))
    (xwidget-resize id (window-pixel-width) (window-pixel-height))
    (set-xwidget-query-on-exit-flag id nil)
    (put-text-property (point) (+ 1 (point))
                       'display (list 'xwidget ':xwidget id))
    (xwidget-webkit-mode)
    (xwidget-webkit-goto-uri id "file:///tmp/reddit.html")
    ))

Reload works with xwidget-webkit-reload