more operations, thanks to Jsoup;

--- a/src/Pure/Thy/html.scala	Sat Mar 11 21:25:24 2023 +0100
+++ b/src/Pure/Thy/html.scala	Sat Mar 11 21:36:25 2023 +0100
@@ -7,6 +7,10 @@
 package isabelle
 
 
+import org.jsoup.nodes.{Entities => Jsoup_Entities, Document => Jsoup_Document}
+import org.jsoup.Jsoup
+
+
 object HTML {
   /* attributes */
 
@@ -255,10 +259,12 @@
     output(List(tree), hidden, structural)
 
 
-  /* input text */
+  /* input */
 
-  def input(text: String): String =
-    org.jsoup.nodes.Entities.unescape(text)
+  def input(text: String): String = Jsoup_Entities.unescape(text)
+
+  def parse_document(html: String): Jsoup_Document = Jsoup.parse(html)
+  def get_document(url: String): Jsoup_Document = Jsoup.connect(url).get()
 
 
   /* messages */