clarified treatment of fragments of Isabelle symbols during bootstrap;
authorwenzelm
Sun Mar 06 16:19:02 2016 +0100 (2016-03-06)
changeset 625298b7bdfc09f3b
parent 62528 c8c532b22947
child 62530 5499461a0203
clarified treatment of fragments of Isabelle symbols during bootstrap;
src/Pure/General/position.ML
src/Pure/General/symbol.ML
src/Pure/General/symbol_pos.ML
src/Pure/Isar/parse.ML
src/Pure/ML/ml_compiler0.ML
src/Pure/Syntax/lexicon.ML
src/Pure/Syntax/syntax_ext.ML
src/Pure/Syntax/syntax_phases.ML
src/Pure/Syntax/syntax_trans.ML
src/Pure/Thy/html.ML
src/Pure/Thy/markdown.ML
src/Pure/library.ML
src/Pure/pure_thy.ML
src/Pure/term.ML
     1.1 --- a/src/Pure/General/position.ML	Sun Mar 06 13:19:19 2016 +0100
     1.2 +++ b/src/Pure/General/position.ML	Sun Mar 06 16:19:02 2016 +0100
     1.3 @@ -208,7 +208,7 @@
     1.4          (SOME i, NONE) => (" ", "(line " ^ Markup.print_int i ^ ")")
     1.5        | (SOME i, SOME name) => (" ", "(line " ^ Markup.print_int i ^ " of " ^ quote name ^ ")")
     1.6        | (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")")
     1.7 -      | _ => if is_reported pos then ("", "\\<here>") else ("", ""));
     1.8 +      | _ => if is_reported pos then ("", "\<here>") else ("", ""));
     1.9    in
    1.10      if null props then ""
    1.11      else s1 ^ Markup.markup (Markup.properties props Markup.position) s2
     2.1 --- a/src/Pure/General/symbol.ML	Sun Mar 06 13:19:19 2016 +0100
     2.2 +++ b/src/Pure/General/symbol.ML	Sun Mar 06 16:19:02 2016 +0100
     2.3 @@ -95,8 +95,8 @@
     2.4  val STX = chr 2;
     2.5  val DEL = chr 127;
     2.6  
     2.7 -val open_ = "\\<open>";
     2.8 -val close = "\\<close>";
     2.9 +val open_ = "\<open>";
    2.10 +val close = "\<close>";
    2.11  
    2.12  val space = chr 32;
    2.13  
    2.14 @@ -110,14 +110,14 @@
    2.15          Vector.sub (small_spaces, n mod 64);
    2.16  end;
    2.17  
    2.18 -val comment = "\\<comment>";
    2.19 +val comment = "\<comment>";
    2.20  
    2.21  fun is_char s = size s = 1;
    2.22  
    2.23  fun is_utf8 s = size s > 0 andalso forall_string (fn c => ord c >= 128) s;
    2.24  
    2.25  fun raw_symbolic s =
    2.26 -  String.isPrefix "\\<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\\<^" s);
    2.27 +  String.isPrefix "\<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\<^" s);
    2.28  
    2.29  fun is_symbolic s =
    2.30    s <> open_ andalso s <> close andalso raw_symbolic s;
    2.31 @@ -129,7 +129,7 @@
    2.32    else is_utf8 s orelse raw_symbolic s;
    2.33  
    2.34  fun is_control s =
    2.35 -  String.isPrefix "\\<^" s andalso String.isSuffix ">" s;
    2.36 +  String.isPrefix "\<^" s andalso String.isSuffix ">" s;
    2.37  
    2.38  
    2.39  (* input source control *)
    2.40 @@ -140,8 +140,8 @@
    2.41  val stopper = Scan.stopper (K eof) is_eof;
    2.42  
    2.43  fun is_malformed s =
    2.44 -  String.isPrefix "\\<" s andalso not (String.isSuffix ">" s)
    2.45 -  orelse s = "\\<>" orelse s = "\\<^>";
    2.46 +  String.isPrefix "\<" s andalso not (String.isSuffix ">" s)
    2.47 +  orelse s = "\<>" orelse s = "\<^>";
    2.48  
    2.49  fun malformed_msg s = "Malformed symbolic character: " ^ quote s;
    2.50  
    2.51 @@ -199,9 +199,9 @@
    2.52  fun encode_raw "" = ""
    2.53    | encode_raw str =
    2.54        let
    2.55 -        val raw0 = enclose "\\<^raw:" ">";
    2.56 +        val raw0 = enclose "\<^raw:" ">";
    2.57          val raw1 = raw0 o implode;
    2.58 -        val raw2 = enclose "\\<^raw" ">" o string_of_int o ord;
    2.59 +        val raw2 = enclose "\<^raw" ">" o string_of_int o ord;
    2.60  
    2.61          fun encode cs = enc (take_prefix raw_chr cs)
    2.62          and enc ([], []) = []
    2.63 @@ -231,11 +231,11 @@
    2.64  (* decode_raw *)
    2.65  
    2.66  fun is_raw s =
    2.67 -  String.isPrefix "\\<^raw" s andalso String.isSuffix ">" s;
    2.68 +  String.isPrefix "\<^raw" s andalso String.isSuffix ">" s;
    2.69  
    2.70  fun decode_raw s =
    2.71    if not (is_raw s) then error (malformed_msg s)
    2.72 -  else if String.isPrefix "\\<^raw:" s then String.substring (s, 7, size s - 8)
    2.73 +  else if String.isPrefix "\<^raw:" s then String.substring (s, 7, size s - 8)
    2.74    else chr (#1 (Library.read_int (raw_explode (String.substring (s, 6, size s - 7)))));
    2.75  
    2.76  
    2.77 @@ -260,144 +260,144 @@
    2.78  local
    2.79    val letter_symbols =
    2.80      Symtab.make_set [
    2.81 -      "\\<A>",
    2.82 -      "\\<B>",
    2.83 -      "\\<C>",
    2.84 -      "\\<D>",
    2.85 -      "\\<E>",
    2.86 -      "\\<F>",
    2.87 -      "\\<G>",
    2.88 -      "\\<H>",
    2.89 -      "\\<I>",
    2.90 -      "\\<J>",
    2.91 -      "\\<K>",
    2.92 -      "\\<L>",
    2.93 -      "\\<M>",
    2.94 -      "\\<N>",
    2.95 -      "\\<O>",
    2.96 -      "\\<P>",
    2.97 -      "\\<Q>",
    2.98 -      "\\<R>",
    2.99 -      "\\<S>",
   2.100 -      "\\<T>",
   2.101 -      "\\<U>",
   2.102 -      "\\<V>",
   2.103 -      "\\<W>",
   2.104 -      "\\<X>",
   2.105 -      "\\<Y>",
   2.106 -      "\\<Z>",
   2.107 -      "\\<a>",
   2.108 -      "\\<b>",
   2.109 -      "\\<c>",
   2.110 -      "\\<d>",
   2.111 -      "\\<e>",
   2.112 -      "\\<f>",
   2.113 -      "\\<g>",
   2.114 -      "\\<h>",
   2.115 -      "\\<i>",
   2.116 -      "\\<j>",
   2.117 -      "\\<k>",
   2.118 -      "\\<l>",
   2.119 -      "\\<m>",
   2.120 -      "\\<n>",
   2.121 -      "\\<o>",
   2.122 -      "\\<p>",
   2.123 -      "\\<q>",
   2.124 -      "\\<r>",
   2.125 -      "\\<s>",
   2.126 -      "\\<t>",
   2.127 -      "\\<u>",
   2.128 -      "\\<v>",
   2.129 -      "\\<w>",
   2.130 -      "\\<x>",
   2.131 -      "\\<y>",
   2.132 -      "\\<z>",
   2.133 -      "\\<AA>",
   2.134 -      "\\<BB>",
   2.135 -      "\\<CC>",
   2.136 -      "\\<DD>",
   2.137 -      "\\<EE>",
   2.138 -      "\\<FF>",
   2.139 -      "\\<GG>",
   2.140 -      "\\<HH>",
   2.141 -      "\\<II>",
   2.142 -      "\\<JJ>",
   2.143 -      "\\<KK>",
   2.144 -      "\\<LL>",
   2.145 -      "\\<MM>",
   2.146 -      "\\<NN>",
   2.147 -      "\\<OO>",
   2.148 -      "\\<PP>",
   2.149 -      "\\<QQ>",
   2.150 -      "\\<RR>",
   2.151 -      "\\<SS>",
   2.152 -      "\\<TT>",
   2.153 -      "\\<UU>",
   2.154 -      "\\<VV>",
   2.155 -      "\\<WW>",
   2.156 -      "\\<XX>",
   2.157 -      "\\<YY>",
   2.158 -      "\\<ZZ>",
   2.159 -      "\\<aa>",
   2.160 -      "\\<bb>",
   2.161 -      "\\<cc>",
   2.162 -      "\\<dd>",
   2.163 -      "\\<ee>",
   2.164 -      "\\<ff>",
   2.165 -      "\\<gg>",
   2.166 -      "\\<hh>",
   2.167 -      "\\<ii>",
   2.168 -      "\\<jj>",
   2.169 -      "\\<kk>",
   2.170 -      "\\<ll>",
   2.171 -      "\\<mm>",
   2.172 -      "\\<nn>",
   2.173 -      "\\<oo>",
   2.174 -      "\\<pp>",
   2.175 -      "\\<qq>",
   2.176 -      "\\<rr>",
   2.177 -      "\\<ss>",
   2.178 -      "\\<tt>",
   2.179 -      "\\<uu>",
   2.180 -      "\\<vv>",
   2.181 -      "\\<ww>",
   2.182 -      "\\<xx>",
   2.183 -      "\\<yy>",
   2.184 -      "\\<zz>",
   2.185 -      "\\<alpha>",
   2.186 -      "\\<beta>",
   2.187 -      "\\<gamma>",
   2.188 -      "\\<delta>",
   2.189 -      "\\<epsilon>",
   2.190 -      "\\<zeta>",
   2.191 -      "\\<eta>",
   2.192 -      "\\<theta>",
   2.193 -      "\\<iota>",
   2.194 -      "\\<kappa>",
   2.195 -      (*"\\<lambda>", sic!*)
   2.196 -      "\\<mu>",
   2.197 -      "\\<nu>",
   2.198 -      "\\<xi>",
   2.199 -      "\\<pi>",
   2.200 -      "\\<rho>",
   2.201 -      "\\<sigma>",
   2.202 -      "\\<tau>",
   2.203 -      "\\<upsilon>",
   2.204 -      "\\<phi>",
   2.205 -      "\\<chi>",
   2.206 -      "\\<psi>",
   2.207 -      "\\<omega>",
   2.208 -      "\\<Gamma>",
   2.209 -      "\\<Delta>",
   2.210 -      "\\<Theta>",
   2.211 -      "\\<Lambda>",
   2.212 -      "\\<Xi>",
   2.213 -      "\\<Pi>",
   2.214 -      "\\<Sigma>",
   2.215 -      "\\<Upsilon>",
   2.216 -      "\\<Phi>",
   2.217 -      "\\<Psi>",
   2.218 -      "\\<Omega>"
   2.219 +      "\<A>",
   2.220 +      "\<B>",
   2.221 +      "\<C>",
   2.222 +      "\<D>",
   2.223 +      "\<E>",
   2.224 +      "\<F>",
   2.225 +      "\<G>",
   2.226 +      "\<H>",
   2.227 +      "\<I>",
   2.228 +      "\<J>",
   2.229 +      "\<K>",
   2.230 +      "\<L>",
   2.231 +      "\<M>",
   2.232 +      "\<N>",
   2.233 +      "\<O>",
   2.234 +      "\<P>",
   2.235 +      "\<Q>",
   2.236 +      "\<R>",
   2.237 +      "\<S>",
   2.238 +      "\<T>",
   2.239 +      "\<U>",
   2.240 +      "\<V>",
   2.241 +      "\<W>",
   2.242 +      "\<X>",
   2.243 +      "\<Y>",
   2.244 +      "\<Z>",
   2.245 +      "\<a>",
   2.246 +      "\<b>",
   2.247 +      "\<c>",
   2.248 +      "\<d>",
   2.249 +      "\<e>",
   2.250 +      "\<f>",
   2.251 +      "\<g>",
   2.252 +      "\<h>",
   2.253 +      "\<i>",
   2.254 +      "\<j>",
   2.255 +      "\<k>",
   2.256 +      "\<l>",
   2.257 +      "\<m>",
   2.258 +      "\<n>",
   2.259 +      "\<o>",
   2.260 +      "\<p>",
   2.261 +      "\<q>",
   2.262 +      "\<r>",
   2.263 +      "\<s>",
   2.264 +      "\<t>",
   2.265 +      "\<u>",
   2.266 +      "\<v>",
   2.267 +      "\<w>",
   2.268 +      "\<x>",
   2.269 +      "\<y>",
   2.270 +      "\<z>",
   2.271 +      "\<AA>",
   2.272 +      "\<BB>",
   2.273 +      "\<CC>",
   2.274 +      "\<DD>",
   2.275 +      "\<EE>",
   2.276 +      "\<FF>",
   2.277 +      "\<GG>",
   2.278 +      "\<HH>",
   2.279 +      "\<II>",
   2.280 +      "\<JJ>",
   2.281 +      "\<KK>",
   2.282 +      "\<LL>",
   2.283 +      "\<MM>",
   2.284 +      "\<NN>",
   2.285 +      "\<OO>",
   2.286 +      "\<PP>",
   2.287 +      "\<QQ>",
   2.288 +      "\<RR>",
   2.289 +      "\<SS>",
   2.290 +      "\<TT>",
   2.291 +      "\<UU>",
   2.292 +      "\<VV>",
   2.293 +      "\<WW>",
   2.294 +      "\<XX>",
   2.295 +      "\<YY>",
   2.296 +      "\<ZZ>",
   2.297 +      "\<aa>",
   2.298 +      "\<bb>",
   2.299 +      "\<cc>",
   2.300 +      "\<dd>",
   2.301 +      "\<ee>",
   2.302 +      "\<ff>",
   2.303 +      "\<gg>",
   2.304 +      "\<hh>",
   2.305 +      "\<ii>",
   2.306 +      "\<jj>",
   2.307 +      "\<kk>",
   2.308 +      "\<ll>",
   2.309 +      "\<mm>",
   2.310 +      "\<nn>",
   2.311 +      "\<oo>",
   2.312 +      "\<pp>",
   2.313 +      "\<qq>",
   2.314 +      "\<rr>",
   2.315 +      "\<ss>",
   2.316 +      "\<tt>",
   2.317 +      "\<uu>",
   2.318 +      "\<vv>",
   2.319 +      "\<ww>",
   2.320 +      "\<xx>",
   2.321 +      "\<yy>",
   2.322 +      "\<zz>",
   2.323 +      "\<alpha>",
   2.324 +      "\<beta>",
   2.325 +      "\<gamma>",
   2.326 +      "\<delta>",
   2.327 +      "\<epsilon>",
   2.328 +      "\<zeta>",
   2.329 +      "\<eta>",
   2.330 +      "\<theta>",
   2.331 +      "\<iota>",
   2.332 +      "\<kappa>",
   2.333 +      (*"\<lambda>", sic!*)
   2.334 +      "\<mu>",
   2.335 +      "\<nu>",
   2.336 +      "\<xi>",
   2.337 +      "\<pi>",
   2.338 +      "\<rho>",
   2.339 +      "\<sigma>",
   2.340 +      "\<tau>",
   2.341 +      "\<upsilon>",
   2.342 +      "\<phi>",
   2.343 +      "\<chi>",
   2.344 +      "\<psi>",
   2.345 +      "\<omega>",
   2.346 +      "\<Gamma>",
   2.347 +      "\<Delta>",
   2.348 +      "\<Theta>",
   2.349 +      "\<Lambda>",
   2.350 +      "\<Xi>",
   2.351 +      "\<Pi>",
   2.352 +      "\<Sigma>",
   2.353 +      "\<Upsilon>",
   2.354 +      "\<Phi>",
   2.355 +      "\<Psi>",
   2.356 +      "\<Omega>"
   2.357      ];
   2.358  in
   2.359  
   2.360 @@ -421,7 +421,7 @@
   2.361  fun is_quasi s = kind s = Quasi;
   2.362  fun is_blank s = kind s = Blank;
   2.363  
   2.364 -val is_block_ctrl = member (op =) ["\\<^bsub>", "\\<^esub>", "\\<^bsup>", "\\<^esup>"];
   2.365 +val is_block_ctrl = member (op =) ["\<^bsub>", "\<^esub>", "\<^bsup>", "\<^esup>"];
   2.366  
   2.367  fun is_quasi_letter s = let val k = kind s in k = Letter orelse k = Quasi end;
   2.368  fun is_letdig s = let val k = kind s in k = Letter orelse k = Digit orelse k = Quasi end;
   2.369 @@ -531,7 +531,7 @@
   2.370  
   2.371  (* bump string -- treat as base 26 or base 1 numbers *)
   2.372  
   2.373 -fun symbolic_end (_ :: "\\<^sub>" :: _) = true
   2.374 +fun symbolic_end (_ :: "\<^sub>" :: _) = true
   2.375    | symbolic_end ("'" :: ss) = symbolic_end ss
   2.376    | symbolic_end (s :: _) = raw_symbolic s
   2.377    | symbolic_end [] = false;
   2.378 @@ -561,8 +561,8 @@
   2.379  
   2.380  fun sym_len s =
   2.381    if not (is_printable s) then (0: int)
   2.382 -  else if String.isPrefix "\\<long" s then 2
   2.383 -  else if String.isPrefix "\\<Long" s then 2
   2.384 +  else if String.isPrefix "\<long" s then 2
   2.385 +  else if String.isPrefix "\<Long" s then 2
   2.386    else 1;
   2.387  
   2.388  fun sym_length ss = fold (fn s => fn n => sym_len s + n) ss 0;
     3.1 --- a/src/Pure/General/symbol_pos.ML	Sun Mar 06 13:19:19 2016 +0100
     3.2 +++ b/src/Pure/General/symbol_pos.ML	Sun Mar 06 16:19:02 2016 +0100
     3.3 @@ -201,9 +201,9 @@
     3.4          ^ quote (content syms) ^ Position.here (#1 (range syms)));
     3.5    in
     3.6      (case syms of
     3.7 -      ("\\<open>", _) :: rest =>
     3.8 +      ("\<open>", _) :: rest =>
     3.9          (case rev rest of
    3.10 -          ("\\<close>", _) :: rrest => rev rrest
    3.11 +          ("\<close>", _) :: rrest => rev rrest
    3.12          | _ => err ())
    3.13      | _ => err ())
    3.14    end;
    3.15 @@ -279,7 +279,7 @@
    3.16  val letter = Scan.one (symbol #> Symbol.is_letter);
    3.17  val letdigs1 = Scan.many1 (symbol #> Symbol.is_letdig);
    3.18  
    3.19 -val sub = Scan.one (symbol #> (fn s => s = "\\<^sub>"));
    3.20 +val sub = Scan.one (symbol #> (fn s => s = "\<^sub>"));
    3.21  
    3.22  in
    3.23  
     4.1 --- a/src/Pure/Isar/parse.ML	Sun Mar 06 13:19:19 2016 +0100
     4.2 +++ b/src/Pure/Isar/parse.ML	Sun Mar 06 16:19:02 2016 +0100
     4.3 @@ -211,7 +211,7 @@
     4.4    group (fn () => "reserved identifier " ^ quote x)
     4.5      (RESET_VALUE (Scan.one (Token.ident_with (fn y => x = y)) >> Token.content_of));
     4.6  
     4.7 -val dots = sym_ident :-- (fn "\\<dots>" => Scan.succeed () | _ => Scan.fail) >> #1;
     4.8 +val dots = sym_ident :-- (fn "\<dots>" => Scan.succeed () | _ => Scan.fail) >> #1;
     4.9  
    4.10  val minus = sym_ident :-- (fn "-" => Scan.succeed () | _ => Scan.fail) >> #1;
    4.11  
     5.1 --- a/src/Pure/ML/ml_compiler0.ML	Sun Mar 06 13:19:19 2016 +0100
     5.2 +++ b/src/Pure/ML/ml_compiler0.ML	Sun Mar 06 16:19:02 2016 +0100
     5.3 @@ -31,13 +31,14 @@
     5.4    if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
     5.5    else s;
     5.6  
     5.7 -fun ml_positions start_line name txt =
     5.8 +fun ml_input start_line name txt =
     5.9    let
    5.10      fun positions line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res =
    5.11            let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")"
    5.12            in positions line cs (s :: res) end
    5.13 -      | positions line (c :: cs) res =
    5.14 -          positions (if c = #"\n" then line + 1 else line) cs (str c :: res)
    5.15 +      | positions line (#"\\" :: #"<" :: cs) res = positions line cs ("\\\\<" :: res)
    5.16 +      | positions line (#"\n" :: cs) res = positions (line + 1) cs ("\n" :: res)
    5.17 +      | positions line (c :: cs) res = positions line cs (str c :: res)
    5.18        | positions _ [] res = rev res;
    5.19    in String.concat (positions start_line (String.explode txt) []) end;
    5.20  
    5.21 @@ -46,7 +47,7 @@
    5.22      val _ = Secure.deny_ml ();
    5.23  
    5.24      val current_line = Unsynchronized.ref line;
    5.25 -    val in_buffer = Unsynchronized.ref (String.explode (ml_positions line file text));
    5.26 +    val in_buffer = Unsynchronized.ref (String.explode (ml_input line file text));
    5.27      val out_buffer = Unsynchronized.ref ([]: string list);
    5.28      fun output () = drop_newline (implode (rev (! out_buffer)));
    5.29  
     6.1 --- a/src/Pure/Syntax/lexicon.ML	Sun Mar 06 13:19:19 2016 +0100
     6.2 +++ b/src/Pure/Syntax/lexicon.ML	Sun Mar 06 16:19:02 2016 +0100
     6.3 @@ -304,7 +304,7 @@
     6.4  
     6.5      fun idxname cs ds = (implode (rev cs), nat 0 ds);
     6.6      fun chop_idx [] ds = idxname [] ds
     6.7 -      | chop_idx (cs as (_ :: "\\<^sub>" :: _)) ds = idxname cs ds
     6.8 +      | chop_idx (cs as (_ :: "\<^sub>" :: _)) ds = idxname cs ds
     6.9        | chop_idx (c :: cs) ds =
    6.10            if Symbol.is_digit c then chop_idx cs (c :: ds)
    6.11            else idxname (c :: cs) ds;
    6.12 @@ -426,10 +426,10 @@
    6.13  
    6.14  fun marker s = (prefix s, unprefix s);
    6.15  
    6.16 -val (mark_class, unmark_class) = marker "\\<^class>";
    6.17 -val (mark_type, unmark_type) = marker "\\<^type>";
    6.18 -val (mark_const, unmark_const) = marker "\\<^const>";
    6.19 -val (mark_fixed, unmark_fixed) = marker "\\<^fixed>";
    6.20 +val (mark_class, unmark_class) = marker "\<^class>";
    6.21 +val (mark_type, unmark_type) = marker "\<^type>";
    6.22 +val (mark_const, unmark_const) = marker "\<^const>";
    6.23 +val (mark_fixed, unmark_fixed) = marker "\<^fixed>";
    6.24  
    6.25  fun unmark {case_class, case_type, case_const, case_fixed, case_default} s =
    6.26    (case try unmark_class s of
     7.1 --- a/src/Pure/Syntax/syntax_ext.ML	Sun Mar 06 13:19:19 2016 +0100
     7.2 +++ b/src/Pure/Syntax/syntax_ext.ML	Sun Mar 06 16:19:02 2016 +0100
     7.3 @@ -140,7 +140,7 @@
     7.4  
     7.5  local
     7.6  
     7.7 -val is_meta = member (op =) ["(", ")", "/", "_", "\\<index>"];
     7.8 +val is_meta = member (op =) ["(", ")", "/", "_", "\<index>"];
     7.9  
    7.10  val scan_delim_char =
    7.11    $$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.not_eof) ||
    7.12 @@ -151,7 +151,7 @@
    7.13  
    7.14  val scan_sym =
    7.15    $$ "_" >> K (Argument ("", 0)) ||
    7.16 -  $$ "\\<index>" >> K index ||
    7.17 +  $$ "\<index>" >> K index ||
    7.18    $$ "(" |-- Scan.many Symbol.is_digit >> (Bg o read_int) ||
    7.19    $$ ")" >> K En ||
    7.20    $$ "/" -- $$ "/" >> K (Brk ~1) ||
    7.21 @@ -168,7 +168,7 @@
    7.22  
    7.23  fun unique_index xsymbs =
    7.24    if length (filter is_index xsymbs) <= 1 then xsymbs
    7.25 -  else error "Duplicate index arguments (\\<index>)";
    7.26 +  else error "Duplicate index arguments (\<index>)";
    7.27  
    7.28  in
    7.29  
     8.1 --- a/src/Pure/Syntax/syntax_phases.ML	Sun Mar 06 13:19:19 2016 +0100
     8.2 +++ b/src/Pure/Syntax/syntax_phases.ML	Sun Mar 06 16:19:02 2016 +0100
     8.3 @@ -179,7 +179,7 @@
     8.4            in [Ast.Constant (Lexicon.mark_type c)] end
     8.5        | asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok
     8.6        | asts_of (Parser.Node ("_position_sort", [Parser.Tip tok])) = asts_of_position "_ofsort" tok
     8.7 -      | asts_of (Parser.Node (a as "\\<^const>Pure.dummy_pattern", [Parser.Tip tok])) =
     8.8 +      | asts_of (Parser.Node (a as "\<^const>Pure.dummy_pattern", [Parser.Tip tok])) =
     8.9            [ast_of_dummy a tok]
    8.10        | asts_of (Parser.Node (a as "_idtdummy", [Parser.Tip tok])) =
    8.11            [ast_of_dummy a tok]
    8.12 @@ -797,7 +797,7 @@
    8.13  
    8.14  (* type propositions *)
    8.15  
    8.16 -fun type_prop_tr' ctxt T [Const ("\\<^const>Pure.sort_constraint", _)] =
    8.17 +fun type_prop_tr' ctxt T [Const ("\<^const>Pure.sort_constraint", _)] =
    8.18        Syntax.const "_sort_constraint" $ term_of_typ (Config.put show_sorts true ctxt) T
    8.19    | type_prop_tr' ctxt T [t] =
    8.20        Syntax.const "_ofclass" $ term_of_typ ctxt T $ t
    8.21 @@ -839,7 +839,7 @@
    8.22      ("_context_xconst", const_ast_tr false)] #>
    8.23    Sign.typed_print_translation
    8.24     [("_type_prop", type_prop_tr'),
    8.25 -    ("\\<^const>Pure.type", type_tr'),
    8.26 +    ("\<^const>Pure.type", type_tr'),
    8.27      ("_type_constraint_", type_constraint_tr')]);
    8.28  
    8.29  
     9.1 --- a/src/Pure/Syntax/syntax_trans.ML	Sun Mar 06 13:19:19 2016 +0100
     9.2 +++ b/src/Pure/Syntax/syntax_trans.ML	Sun Mar 06 16:19:02 2016 +0100
     9.3 @@ -102,7 +102,7 @@
     9.4  fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys)
     9.5    | tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts);
     9.6  
     9.7 -fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
     9.8 +fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
     9.9    | bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts);
    9.10  
    9.11  
    9.12 @@ -152,18 +152,18 @@
    9.13  
    9.14  fun mk_type ty =
    9.15    Syntax.const "_constrain" $
    9.16 -    Syntax.const "\\<^const>Pure.type" $ (Syntax.const "\\<^type>itself" $ ty);
    9.17 +    Syntax.const "\<^const>Pure.type" $ (Syntax.const "\<^type>itself" $ ty);
    9.18  
    9.19  fun ofclass_tr [ty, cls] = cls $ mk_type ty
    9.20    | ofclass_tr ts = raise TERM ("ofclass_tr", ts);
    9.21  
    9.22 -fun sort_constraint_tr [ty] = Syntax.const "\\<^const>Pure.sort_constraint" $ mk_type ty
    9.23 +fun sort_constraint_tr [ty] = Syntax.const "\<^const>Pure.sort_constraint" $ mk_type ty
    9.24    | sort_constraint_tr ts = raise TERM ("sort_constraint_tr", ts);
    9.25  
    9.26  
    9.27  (* meta propositions *)
    9.28  
    9.29 -fun aprop_tr [t] = Syntax.const "_constrain" $ t $ Syntax.const "\\<^type>prop"
    9.30 +fun aprop_tr [t] = Syntax.const "_constrain" $ t $ Syntax.const "\<^type>prop"
    9.31    | aprop_tr ts = raise TERM ("aprop_tr", ts);
    9.32  
    9.33  
    9.34 @@ -174,7 +174,7 @@
    9.35          (case Ast.unfold_ast_p "_asms" asms of
    9.36            (asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm']
    9.37          | _ => raise Ast.AST ("bigimpl_ast_tr", asts))
    9.38 -      in Ast.fold_ast_p "\\<^const>Pure.imp" (prems, concl) end
    9.39 +      in Ast.fold_ast_p "\<^const>Pure.imp" (prems, concl) end
    9.40    | bigimpl_ast_tr asts = raise Ast.AST ("bigimpl_ast_tr", asts);
    9.41  
    9.42  
    9.43 @@ -273,7 +273,7 @@
    9.44  fun fun_ast_tr' asts =
    9.45    if no_brackets () orelse no_type_brackets () then raise Match
    9.46    else
    9.47 -    (case Ast.unfold_ast_p "\\<^type>fun" (Ast.Appl (Ast.Constant "\\<^type>fun" :: asts)) of
    9.48 +    (case Ast.unfold_ast_p "\<^type>fun" (Ast.Appl (Ast.Constant "\<^type>fun" :: asts)) of
    9.49        (dom as _ :: _ :: _, cod)
    9.50          => Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
    9.51      | _ => raise Match);
    9.52 @@ -389,8 +389,8 @@
    9.53  fun impl_ast_tr' asts =
    9.54    if no_brackets () then raise Match
    9.55    else
    9.56 -    (case Ast.unfold_ast_p "\\<^const>Pure.imp"
    9.57 -        (Ast.Appl (Ast.Constant "\\<^const>Pure.imp" :: asts)) of
    9.58 +    (case Ast.unfold_ast_p "\<^const>Pure.imp"
    9.59 +        (Ast.Appl (Ast.Constant "\<^const>Pure.imp" :: asts)) of
    9.60        (prems as _ :: _ :: _, concl) =>
    9.61          let
    9.62            val (asms, asm) = split_last prems;
    9.63 @@ -501,11 +501,11 @@
    9.64    ("_struct", struct_tr)];
    9.65  
    9.66  val pure_print_ast_translation =
    9.67 - [("\\<^type>fun", fn _ => fun_ast_tr'),
    9.68 + [("\<^type>fun", fn _ => fun_ast_tr'),
    9.69    ("_abs", fn _ => abs_ast_tr'),
    9.70    ("_idts", fn _ => idtyp_ast_tr' "_idts"),
    9.71    ("_pttrns", fn _ => idtyp_ast_tr' "_pttrns"),
    9.72 -  ("\\<^const>Pure.imp", fn _ => impl_ast_tr'),
    9.73 +  ("\<^const>Pure.imp", fn _ => impl_ast_tr'),
    9.74    ("_index", fn _ => index_ast_tr'),
    9.75    ("_struct", struct_ast_tr')];
    9.76  
    10.1 --- a/src/Pure/Thy/html.ML	Sun Mar 06 13:19:19 2016 +0100
    10.2 +++ b/src/Pure/Thy/html.ML	Sun Mar 06 16:19:02 2016 +0100
    10.3 @@ -39,10 +39,10 @@
    10.4      val mapping =
    10.5        map (apsnd (fn c => "&#" ^ Markup.print_int c ^ ";")) codes @
    10.6         [("'", "&#39;"),
    10.7 -        ("\\<^bsub>", hidden "&#8664;" ^ "<sub>"),
    10.8 -        ("\\<^esub>", hidden "&#8665;" ^ "</sub>"),
    10.9 -        ("\\<^bsup>", hidden "&#8663;" ^ "<sup>"),
   10.10 -        ("\\<^esup>", hidden "&#8662;" ^ "</sup>")];
   10.11 +        ("\<^bsub>", hidden "&#8664;" ^ "<sub>"),
   10.12 +        ("\<^esub>", hidden "&#8665;" ^ "</sub>"),
   10.13 +        ("\<^bsup>", hidden "&#8663;" ^ "<sup>"),
   10.14 +        ("\<^esup>", hidden "&#8662;" ^ "</sup>")];
   10.15    in Symbols (fold Symtab.update mapping Symtab.empty) end;
   10.16  
   10.17  val no_symbols = make_symbols [];
   10.18 @@ -70,9 +70,9 @@
   10.19        let
   10.20          val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss));
   10.21          val (s, r) =
   10.22 -          if s1 = "\\<^sub>" then (output_sub symbols "&#8681;" s2, ss)
   10.23 -          else if s1 = "\\<^sup>" then (output_sup symbols "&#8679;" s2, ss)
   10.24 -          else if s1 = "\\<^bold>" then (output_bold symbols "&#10073;" s2, ss)
   10.25 +          if s1 = "\<^sub>" then (output_sub symbols "&#8681;" s2, ss)
   10.26 +          else if s1 = "\<^sup>" then (output_sup symbols "&#8679;" s2, ss)
   10.27 +          else if s1 = "\<^bold>" then (output_bold symbols "&#10073;" s2, ss)
   10.28            else (output_sym symbols s1, rest);
   10.29        in output_syms symbols r (s :: result) end;
   10.30  
   10.31 @@ -120,19 +120,19 @@
   10.32  (* document *)
   10.33  
   10.34  fun begin_document symbols title =
   10.35 -  "<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n\
   10.36 -  \<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" \
   10.37 -  \\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n\
   10.38 -  \<html xmlns=\"http://www.w3.org/1999/xhtml\">\n\
   10.39 -  \<head>\n\
   10.40 -  \<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n\
   10.41 -  \<title>" ^ output symbols (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\
   10.42 -  \<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n\
   10.43 -  \</head>\n\
   10.44 -  \\n\
   10.45 -  \<body>\n\
   10.46 -  \<div class=\"head\">\
   10.47 -  \<h1>" ^ output symbols title ^ "</h1>\n";
   10.48 +  "<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n" ^
   10.49 +  "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" " ^
   10.50 +  "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n" ^
   10.51 +  "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n" ^
   10.52 +  "<head>\n" ^
   10.53 +  "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n" ^
   10.54 +  "<title>" ^ output symbols (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n" ^
   10.55 +  "<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n" ^
   10.56 +  "</head>\n" ^
   10.57 +  "\n" ^
   10.58 +  "<body>\n" ^
   10.59 +  "<div class=\"head\">" ^
   10.60 +  "<h1>" ^ output symbols title ^ "</h1>\n";
   10.61  
   10.62  val end_document = "\n</div>\n</body>\n</html>\n";
   10.63  
    11.1 --- a/src/Pure/Thy/markdown.ML	Sun Mar 06 13:19:19 2016 +0100
    11.2 +++ b/src/Pure/Thy/markdown.ML	Sun Mar 06 16:19:02 2016 +0100
    11.3 @@ -49,7 +49,7 @@
    11.4  
    11.5  val kinds = [("item", Itemize), ("enum", Enumerate), ("descr", Description)];
    11.6  
    11.7 -val is_control = member (op =) ["\\<^item>", "\\<^enum>", "\\<^descr>"];
    11.8 +val is_control = member (op =) ["\<^item>", "\<^enum>", "\<^descr>"];
    11.9  
   11.10  
   11.11  (* document lines *)
    12.1 --- a/src/Pure/library.ML	Sun Mar 06 13:19:19 2016 +0100
    12.2 +++ b/src/Pure/library.ML	Sun Mar 06 16:19:02 2016 +0100
    12.3 @@ -693,7 +693,7 @@
    12.4  (*simple quoting (does not escape special chars)*)
    12.5  val quote = enclose "\"" "\"";
    12.6  
    12.7 -val cartouche = enclose "\\<open>" "\\<close>";
    12.8 +val cartouche = enclose "\<open>" "\<close>";
    12.9  
   12.10  val space_implode = String.concatWith;
   12.11  
    13.1 --- a/src/Pure/pure_thy.ML	Sun Mar 06 13:19:19 2016 +0100
    13.2 +++ b/src/Pure/pure_thy.ML	Sun Mar 06 16:19:02 2016 +0100
    13.3 @@ -108,12 +108,12 @@
    13.4      ("_tappl",      typ "type => types => type_name => type", Delimfix "((1'(_,/ _')) _)"),
    13.5      ("",            typ "type => types",               Delimfix "_"),
    13.6      ("_types",      typ "type => types => types",      Delimfix "_,/ _"),
    13.7 -    ("\\<^type>fun", typ "type => type => type",       Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
    13.8 -    ("_bracket",    typ "types => type => type",       Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
    13.9 +    ("\<^type>fun", typ "type => type => type",        Mixfix ("(_/ \<Rightarrow> _)", [1, 0], 0)),
   13.10 +    ("_bracket",    typ "types => type => type",       Mixfix ("([_]/ \<Rightarrow> _)", [0, 0], 0)),
   13.11      ("",            typ "type => type",                Delimfix "'(_')"),
   13.12 -    ("\\<^type>dummy", typ "type",                     Delimfix "'_"),
   13.13 +    ("\<^type>dummy", typ "type",                      Delimfix "'_"),
   13.14      ("_type_prop",  typ "'a",                          NoSyn),
   13.15 -    ("_lambda",     typ "pttrns => 'a => logic",       Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
   13.16 +    ("_lambda",     typ "pttrns => 'a => logic",       Mixfix ("(3\<lambda>_./ _)", [0, 3], 3)),
   13.17      ("_abs",        typ "'a",                          NoSyn),
   13.18      ("",            typ "'a => args",                  Delimfix "_"),
   13.19      ("_args",       typ "'a => args => args",          Delimfix "_,/ _"),
   13.20 @@ -131,26 +131,26 @@
   13.21      ("",            typ "id_position => aprop",        Delimfix "_"),
   13.22      ("",            typ "longid_position => aprop",    Delimfix "_"),
   13.23      ("",            typ "var_position => aprop",       Delimfix "_"),
   13.24 -    ("_DDDOT",      typ "aprop",                       Delimfix "\\<dots>"),
   13.25 +    ("_DDDOT",      typ "aprop",                       Delimfix "\<dots>"),
   13.26      ("_aprop",      typ "aprop => prop",               Delimfix "PROP _"),
   13.27      ("_asm",        typ "prop => asms",                Delimfix "_"),
   13.28      ("_asms",       typ "prop => asms => asms",        Delimfix "_;/ _"),
   13.29 -    ("_bigimpl",    typ "asms => prop => prop",        Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
   13.30 +    ("_bigimpl",    typ "asms => prop => prop",        Mixfix ("((1\<lbrakk>_\<rbrakk>)/ \<Longrightarrow> _)", [0, 1], 1)),
   13.31      ("_ofclass",    typ "type => logic => prop",       Delimfix "(1OFCLASS/(1'(_,/ _')))"),
   13.32      ("_mk_ofclass", typ "dummy",                       NoSyn),
   13.33      ("_TYPE",       typ "type => logic",               Delimfix "(1TYPE/(1'(_')))"),
   13.34      ("",            typ "id_position => logic",        Delimfix "_"),
   13.35      ("",            typ "longid_position => logic",    Delimfix "_"),
   13.36      ("",            typ "var_position => logic",       Delimfix "_"),
   13.37 -    ("_DDDOT",      typ "logic",                       Delimfix "\\<dots>"),
   13.38 +    ("_DDDOT",      typ "logic",                       Delimfix "\<dots>"),
   13.39      ("_strip_positions", typ "'a", NoSyn),
   13.40      ("_position",   typ "num_token => num_position",   Delimfix "_"),
   13.41      ("_position",   typ "float_token => float_position", Delimfix "_"),
   13.42      ("_constify",   typ "num_position => num_const",   Delimfix "_"),
   13.43      ("_constify",   typ "float_position => float_const", Delimfix "_"),
   13.44 -    ("_index",      typ "logic => index",              Delimfix "(00\\<^bsub>_\\<^esub>)"),
   13.45 +    ("_index",      typ "logic => index",              Delimfix "(00\<^bsub>_\<^esub>)"),
   13.46      ("_indexdefault", typ "index",                     Delimfix ""),
   13.47 -    ("_indexvar",   typ "index",                       Delimfix "'\\<index>"),
   13.48 +    ("_indexvar",   typ "index",                       Delimfix "'\<index>"),
   13.49      ("_struct",     typ "index => logic",              NoSyn),
   13.50      ("_update_name", typ "idt",                        NoSyn),
   13.51      ("_constrainAbs", typ "'a",                        NoSyn),
   13.52 @@ -189,9 +189,9 @@
   13.53    #> Sign.add_syntax ("", false)
   13.54     [(const "Pure.prop", typ "prop => prop", Mixfix ("_", [0], 0))]
   13.55    #> Sign.add_consts
   13.56 -   [(qualify (Binding.make ("eq", @{here})), typ "'a => 'a => prop", Infix ("\\<equiv>", 2)),
   13.57 -    (qualify (Binding.make ("imp", @{here})), typ "prop => prop => prop", Infixr ("\\<Longrightarrow>", 1)),
   13.58 -    (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", Binder ("\\<And>", 0, 0)),
   13.59 +   [(qualify (Binding.make ("eq", @{here})), typ "'a => 'a => prop", Infix ("\<equiv>", 2)),
   13.60 +    (qualify (Binding.make ("imp", @{here})), typ "prop => prop => prop", Infixr ("\<Longrightarrow>", 1)),
   13.61 +    (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", Binder ("\<And>", 0, 0)),
   13.62      (qualify (Binding.make ("prop", @{here})), typ "prop => prop", NoSyn),
   13.63      (qualify (Binding.make ("type", @{here})), typ "'a itself", NoSyn),
   13.64      (qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", Delimfix "'_")]
    14.1 --- a/src/Pure/term.ML	Sun Mar 06 13:19:19 2016 +0100
    14.2 +++ b/src/Pure/term.ML	Sun Mar 06 16:19:02 2016 +0100
    14.3 @@ -986,7 +986,7 @@
    14.4      val idx = string_of_int i;
    14.5      val dot =
    14.6        (case rev (Symbol.explode x) of
    14.7 -        _ :: "\\<^sub>" :: _ => false
    14.8 +        _ :: "\<^sub>" :: _ => false
    14.9        | c :: _ => Symbol.is_digit c
   14.10        | _ => true);
   14.11    in