# HG changeset patch
# User wenzelm
# Date 1552942251 -3600
# Node ID 5f67c5e457e34034ba91b3175ca77103416783de
# Parent  eddcc7c726f3e57e73c59d328e19a3455874f457# Parent  79c8ff387ed1cdc380fb52da194db022aa59ac51
merged

diff -r eddcc7c726f3 -r 5f67c5e457e3 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Mon Mar 18 15:35:34 2019 +0000
+++ b/src/Pure/PIDE/headless.scala	Mon Mar 18 21:50:51 2019 +0100
@@ -152,6 +152,7 @@
       theories: List[String],
       qualifier: String = Sessions.DRAFT,
       master_dir: String = "",
+      unicode_symbols: Boolean = false,
       check_delay: Time = default_check_delay,
       check_limit: Int = default_check_limit,
       watchdog_timeout: Time = default_watchdog_timeout,
@@ -263,7 +264,7 @@
 
       try {
         session.commands_changed += consumer
-        resources.load_theories(session, id, dep_theories, dep_files, progress)
+        resources.load_theories(session, id, dep_theories, dep_files, unicode_symbols, progress)
         use_theories_state.value.await_result
         check_progress.cancel
       }
@@ -535,6 +536,7 @@
       id: UUID.T,
       dep_theories: List[Document.Node.Name],
       dep_files: List[Document.Node.Name],
+      unicode_symbols: Boolean,
       progress: Progress)
     {
       val loaded_theories =
@@ -544,7 +546,8 @@
           if (!node_name.is_theory) error("Not a theory file: " + path)
 
           progress.expose_interrupt()
-          val text = File.read(path)
+          val text0 = File.read(path)
+          val text = if (unicode_symbols) Symbol.decode(text0) else text0
           val node_header = resources.check_thy_reader(node_name, Scan.char_reader(text))
           new Resources.Theory(node_name, node_header, text, true)
         }
diff -r eddcc7c726f3 -r 5f67c5e457e3 src/Pure/Thy/thy_element.scala
--- a/src/Pure/Thy/thy_element.scala	Mon Mar 18 15:35:34 2019 +0000
+++ b/src/Pure/Thy/thy_element.scala	Mon Mar 18 21:50:51 2019 +0100
@@ -30,6 +30,13 @@
         case Some((_, qed)) => Iterator(head, qed)
       }
 
+    def proof_start: Option[A] =
+      proof match {
+        case None => None
+        case Some((Nil, qed)) => Some(qed)
+        case Some((start :: _, _)) => Some(start.head)
+      }
+
     def last: A =
       proof match {
         case None => head
diff -r eddcc7c726f3 -r 5f67c5e457e3 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Mon Mar 18 15:35:34 2019 +0000
+++ b/src/Pure/Tools/dump.scala	Mon Mar 18 21:50:51 2019 +0100
@@ -105,6 +105,7 @@
   def session(
     deps: Sessions.Deps,
     resources: Headless.Resources,
+    unicode_symbols: Boolean = false,
     process_theory: Args => Unit,
     progress: Progress = No_Progress)
   {
@@ -168,7 +169,10 @@
     try {
       val use_theories = resources.used_theories(deps).map(_.theory)
       val use_theories_result =
-        session.use_theories(use_theories, progress = progress, commit = Some(Consumer.apply _))
+        session.use_theories(use_theories,
+          unicode_symbols = unicode_symbols,
+          progress = progress,
+          commit = Some(Consumer.apply _))
 
       val bad_theories = Consumer.shutdown()
       val bad_msgs =