# 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 + +"""