# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1716918709 -7200
# Node ID ca9a402735b4c2d04ce00876093d00c0294d650d
# Parent  03c058592c58167a9fb235973aa6e42645f79b84
proper html script tag: source code must not be escaped;

diff -r 03c058592c58 -r ca9a402735b4 src/Pure/General/html.scala
--- a/src/Pure/General/html.scala	Tue May 28 19:51:09 2024 +0200
+++ b/src/Pure/General/html.scala	Tue May 28 19:51:49 2024 +0200
@@ -93,7 +93,7 @@
     XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> href)), Nil)
   def style_file(path: Path): XML.Elem = style_file(Url.print_file(path.file))
 
-  def script(s: String): XML.Elem = XML.elem("script", text(s))
+  def script(s: String): XML.Elem = XML.elem("script", List(raw(text(s))))
   def script_file(href: String): XML.Elem = XML.Elem(Markup("script", List("src" -> href)), Nil)
   def script_file(path: Path): XML.Elem = script_file(Url.print_file(path.file))