# HG changeset patch
# User wenzelm
# Date 1550151881 -3600
# Node ID 9efccbad7d425d10cf2bfaccffa8ff87c057b956
# Parent a24865b6262f6b8a63ff97c03327d7a852cdb9bd
uniform XML header;
diff -r a24865b6262f -r 9efccbad7d42 src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML Wed Feb 13 11:25:23 2019 +0100
+++ b/src/Pure/PIDE/xml.ML Thu Feb 14 14:44:41 2019 +0100
@@ -122,7 +122,7 @@
(** string representation **)
-val header = "\n";
+val header = "\n";
(* escaped text *)
diff -r a24865b6262f -r 9efccbad7d42 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala Wed Feb 13 11:25:23 2019 +0100
+++ b/src/Pure/PIDE/xml.scala Thu Feb 14 14:44:41 2019 +0100
@@ -99,6 +99,8 @@
/** string representation **/
+ val header: String = "\n"
+
def output_char(c: Char, s: StringBuilder)
{
c match {
diff -r a24865b6262f -r 9efccbad7d42 src/Pure/Thy/html.ML
--- a/src/Pure/Thy/html.ML Wed Feb 13 11:25:23 2019 +0100
+++ b/src/Pure/Thy/html.ML Thu Feb 14 14:44:41 2019 +0100
@@ -126,7 +126,7 @@
(* document *)
fun begin_document symbols title =
- "\n" ^
+ XML.header ^
"\n" ^
"\n" ^
diff -r a24865b6262f -r 9efccbad7d42 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala Wed Feb 13 11:25:23 2019 +0100
+++ b/src/Pure/Thy/html.scala Thu Feb 14 14:44:41 2019 +0100
@@ -324,8 +324,8 @@
/* document */
val header: String =
- """
-
+ XML.header +
+ """
"""
val head_meta: XML.Elem =
diff -r a24865b6262f -r 9efccbad7d42 src/Pure/Tools/main.scala
--- a/src/Pure/Tools/main.scala Wed Feb 13 11:25:23 2019 +0100
+++ b/src/Pure/Tools/main.scala Thu Feb 14 14:44:41 2019 +0100
@@ -55,8 +55,8 @@
File.write(settings_dir + Path.explode("DockableWindowManager/perspective-view0.xml"),
"""""")
File.write(settings_dir + Path.explode("perspective.xml"),
- """
-
+ XML.header +
+"""