# HG changeset patch
# User wenzelm
# Date 1678566985 -3600
# Node ID 58576816d3046b95573ec929d3df1157073342b4
# Parent  6d0985955872d9395ea47a0340978b331ebb9284
more operations, thanks to Jsoup;

diff -r 6d0985955872 -r 58576816d304 src/Pure/Thy/html.scala
--- 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 */