# HG changeset patch
# User wenzelm
# Date 1552939586 -3600
# Node ID 79c8ff387ed1cdc380fb52da194db022aa59ac51
# Parent  7837309d633a6e5f19d1a39b02c0b8ec811ceea6
support unicode_symbols in input source;

diff -r 7837309d633a -r 79c8ff387ed1 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Mon Mar 18 21:05:34 2019 +0100
+++ b/src/Pure/PIDE/headless.scala	Mon Mar 18 21:06:26 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 7837309d633a -r 79c8ff387ed1 src/Pure/Tools/dump.scala
--- a/src/Pure/Tools/dump.scala	Mon Mar 18 21:05:34 2019 +0100
+++ b/src/Pure/Tools/dump.scala	Mon Mar 18 21:06:26 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 =