Symbol.STX, Symbol.DEL;
authorwenzelm
Thu Apr 03 16:03:57 2008 +0200 (2008-04-03)
changeset 26527c392354a1b79
parent 26526 d1557acb9ef9
child 26528 944f9bf26d2d
Symbol.STX, Symbol.DEL;
src/Pure/Tools/isabelle_process.ML
     1.1 --- a/src/Pure/Tools/isabelle_process.ML	Thu Apr 03 16:03:56 2008 +0200
     1.2 +++ b/src/Pure/Tools/isabelle_process.ML	Thu Apr 03 16:03:57 2008 +0200
     1.3 @@ -65,10 +65,7 @@
     1.4  
     1.5  (* message markup *)
     1.6  
     1.7 -val STX = chr 2;
     1.8 -val DEL = chr 127;
     1.9 -
    1.10 -fun special ch = STX ^ ch;
    1.11 +fun special ch = Symbol.STX ^ ch;
    1.12  val special_sep = special ",";
    1.13  val special_end = special ".";
    1.14  
    1.15 @@ -77,7 +74,7 @@
    1.16  fun print_props props =
    1.17    let
    1.18      val clean = translate_string (fn c =>
    1.19 -      if c = STX orelse c = "\n" orelse c = "\r" then DEL else c);
    1.20 +      if c = Symbol.STX orelse c = "\n" orelse c = "\r" then Symbol.DEL else c);
    1.21    in implode (map (fn (x, y) => clean x ^ "=" ^ clean y ^ special_sep ^ "\n") props) end;
    1.22  
    1.23  fun get_pos (elem as XML.Elem (name, atts, ts)) =
    1.24 @@ -100,7 +97,7 @@
    1.25        | SOME xml =>
    1.26            (if print_mode_active full_markupN then XML.header ^ txt1 else XML.plain_content xml,
    1.27              the_default Position.none (get_pos xml)))
    1.28 -      |>> translate_string (fn c => if c = STX then DEL else c);
    1.29 +      |>> translate_string (fn c => if c = Symbol.STX then Symbol.DEL else c);
    1.30      val props =
    1.31        Position.properties_of (Position.thread_data ())
    1.32        |> Position.default_properties pos;