# HG changeset patch
# User wenzelm
# Date 1207231437 -7200
# Node ID c392354a1b798568f64df7e46c7486c710450a97
# Parent  d1557acb9ef91e92a8b5f3f369e7182c3fef8b9d
Symbol.STX, Symbol.DEL;

diff -r d1557acb9ef9 -r c392354a1b79 src/Pure/Tools/isabelle_process.ML
--- a/src/Pure/Tools/isabelle_process.ML	Thu Apr 03 16:03:56 2008 +0200
+++ b/src/Pure/Tools/isabelle_process.ML	Thu Apr 03 16:03:57 2008 +0200
@@ -65,10 +65,7 @@
 
 (* message markup *)
 
-val STX = chr 2;
-val DEL = chr 127;
-
-fun special ch = STX ^ ch;
+fun special ch = Symbol.STX ^ ch;
 val special_sep = special ",";
 val special_end = special ".";
 
@@ -77,7 +74,7 @@
 fun print_props props =
   let
     val clean = translate_string (fn c =>
-      if c = STX orelse c = "\n" orelse c = "\r" then DEL else c);
+      if c = Symbol.STX orelse c = "\n" orelse c = "\r" then Symbol.DEL else c);
   in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end;
 
 fun get_pos (elem as XML.Elem (name, atts, ts)) =
@@ -100,7 +97,7 @@
       | SOME xml =>
           (if print_mode_active full_markupN then XML.header ^ txt1 else XML.plain_content xml,
             the_default Position.none (get_pos xml)))
-      |>> translate_string (fn c => if c = STX then DEL else c);
+      |>> translate_string (fn c => if c = Symbol.STX then Symbol.DEL else c);
     val props =
       Position.properties_of (Position.thread_data ())
       |> Position.default_properties pos;