--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Sun Mar 06 20:39:19 2016 +0100
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Mon Mar 07 08:14:18 2016 +0100
@@ -279,7 +279,6 @@
let
val output_value = the_default "NONE"
(try (snd o split_last o filter_out (fn s => s = "") o split_lines) response)
- |> translate_string (fn s => if s = "\\" then "\\\\" else s)
val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))";
val ctxt' = ctxt
--- a/src/Pure/General/bytes.scala Sun Mar 06 20:39:19 2016 +0100
+++ b/src/Pure/General/bytes.scala Mon Mar 07 08:14:18 2016 +0100
@@ -20,7 +20,7 @@
val str = s.toString
if (str.isEmpty) empty
else {
- val b = str.getBytes(UTF8.charset)
+ val b = UTF8.bytes(str)
new Bytes(b, 0, b.length)
}
}
--- a/src/Pure/General/position.ML Sun Mar 06 20:39:19 2016 +0100
+++ b/src/Pure/General/position.ML Mon Mar 07 08:14:18 2016 +0100
@@ -208,7 +208,7 @@
(SOME i, NONE) => (" ", "(line " ^ Markup.print_int i ^ ")")
| (SOME i, SOME name) => (" ", "(line " ^ Markup.print_int i ^ " of " ^ quote name ^ ")")
| (NONE, SOME name) => (" ", "(file " ^ quote name ^ ")")
- | _ => if is_reported pos then ("", "\\<here>") else ("", ""));
+ | _ => if is_reported pos then ("", "\<here>") else ("", ""));
in
if null props then ""
else s1 ^ Markup.markup (Markup.properties props Markup.position) s2
--- a/src/Pure/General/symbol.ML Sun Mar 06 20:39:19 2016 +0100
+++ b/src/Pure/General/symbol.ML Mon Mar 07 08:14:18 2016 +0100
@@ -95,8 +95,8 @@
val STX = chr 2;
val DEL = chr 127;
-val open_ = "\\<open>";
-val close = "\\<close>";
+val open_ = "\<open>";
+val close = "\<close>";
val space = chr 32;
@@ -110,14 +110,14 @@
Vector.sub (small_spaces, n mod 64);
end;
-val comment = "\\<comment>";
+val comment = "\<comment>";
fun is_char s = size s = 1;
fun is_utf8 s = size s > 0 andalso forall_string (fn c => ord c >= 128) s;
fun raw_symbolic s =
- String.isPrefix "\\<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\\<^" s);
+ String.isPrefix "\<" s andalso String.isSuffix ">" s andalso not (String.isPrefix "\<^" s);
fun is_symbolic s =
s <> open_ andalso s <> close andalso raw_symbolic s;
@@ -129,7 +129,7 @@
else is_utf8 s orelse raw_symbolic s;
fun is_control s =
- String.isPrefix "\\<^" s andalso String.isSuffix ">" s;
+ String.isPrefix "\<^" s andalso String.isSuffix ">" s;
(* input source control *)
@@ -140,8 +140,8 @@
val stopper = Scan.stopper (K eof) is_eof;
fun is_malformed s =
- String.isPrefix "\\<" s andalso not (String.isSuffix ">" s)
- orelse s = "\\<>" orelse s = "\\<^>";
+ String.isPrefix "\<" s andalso not (String.isSuffix ">" s)
+ orelse s = "\<>" orelse s = "\<^>";
fun malformed_msg s = "Malformed symbolic character: " ^ quote s;
@@ -199,9 +199,9 @@
fun encode_raw "" = ""
| encode_raw str =
let
- val raw0 = enclose "\\<^raw:" ">";
+ val raw0 = enclose "\<^raw:" ">";
val raw1 = raw0 o implode;
- val raw2 = enclose "\\<^raw" ">" o string_of_int o ord;
+ val raw2 = enclose "\<^raw" ">" o string_of_int o ord;
fun encode cs = enc (take_prefix raw_chr cs)
and enc ([], []) = []
@@ -231,11 +231,11 @@
(* decode_raw *)
fun is_raw s =
- String.isPrefix "\\<^raw" s andalso String.isSuffix ">" s;
+ String.isPrefix "\<^raw" s andalso String.isSuffix ">" s;
fun decode_raw s =
if not (is_raw s) then error (malformed_msg s)
- else if String.isPrefix "\\<^raw:" s then String.substring (s, 7, size s - 8)
+ else if String.isPrefix "\<^raw:" s then String.substring (s, 7, size s - 8)
else chr (#1 (Library.read_int (raw_explode (String.substring (s, 6, size s - 7)))));
@@ -260,144 +260,144 @@
local
val letter_symbols =
Symtab.make_set [
- "\\<A>",
- "\\<B>",
- "\\<C>",
- "\\<D>",
- "\\<E>",
- "\\<F>",
- "\\<G>",
- "\\<H>",
- "\\<I>",
- "\\<J>",
- "\\<K>",
- "\\<L>",
- "\\<M>",
- "\\<N>",
- "\\<O>",
- "\\<P>",
- "\\<Q>",
- "\\<R>",
- "\\<S>",
- "\\<T>",
- "\\<U>",
- "\\<V>",
- "\\<W>",
- "\\<X>",
- "\\<Y>",
- "\\<Z>",
- "\\<a>",
- "\\<b>",
- "\\<c>",
- "\\<d>",
- "\\<e>",
- "\\<f>",
- "\\<g>",
- "\\<h>",
- "\\<i>",
- "\\<j>",
- "\\<k>",
- "\\<l>",
- "\\<m>",
- "\\<n>",
- "\\<o>",
- "\\<p>",
- "\\<q>",
- "\\<r>",
- "\\<s>",
- "\\<t>",
- "\\<u>",
- "\\<v>",
- "\\<w>",
- "\\<x>",
- "\\<y>",
- "\\<z>",
- "\\<AA>",
- "\\<BB>",
- "\\<CC>",
- "\\<DD>",
- "\\<EE>",
- "\\<FF>",
- "\\<GG>",
- "\\<HH>",
- "\\<II>",
- "\\<JJ>",
- "\\<KK>",
- "\\<LL>",
- "\\<MM>",
- "\\<NN>",
- "\\<OO>",
- "\\<PP>",
- "\\<QQ>",
- "\\<RR>",
- "\\<SS>",
- "\\<TT>",
- "\\<UU>",
- "\\<VV>",
- "\\<WW>",
- "\\<XX>",
- "\\<YY>",
- "\\<ZZ>",
- "\\<aa>",
- "\\<bb>",
- "\\<cc>",
- "\\<dd>",
- "\\<ee>",
- "\\<ff>",
- "\\<gg>",
- "\\<hh>",
- "\\<ii>",
- "\\<jj>",
- "\\<kk>",
- "\\<ll>",
- "\\<mm>",
- "\\<nn>",
- "\\<oo>",
- "\\<pp>",
- "\\<qq>",
- "\\<rr>",
- "\\<ss>",
- "\\<tt>",
- "\\<uu>",
- "\\<vv>",
- "\\<ww>",
- "\\<xx>",
- "\\<yy>",
- "\\<zz>",
- "\\<alpha>",
- "\\<beta>",
- "\\<gamma>",
- "\\<delta>",
- "\\<epsilon>",
- "\\<zeta>",
- "\\<eta>",
- "\\<theta>",
- "\\<iota>",
- "\\<kappa>",
- (*"\\<lambda>", sic!*)
- "\\<mu>",
- "\\<nu>",
- "\\<xi>",
- "\\<pi>",
- "\\<rho>",
- "\\<sigma>",
- "\\<tau>",
- "\\<upsilon>",
- "\\<phi>",
- "\\<chi>",
- "\\<psi>",
- "\\<omega>",
- "\\<Gamma>",
- "\\<Delta>",
- "\\<Theta>",
- "\\<Lambda>",
- "\\<Xi>",
- "\\<Pi>",
- "\\<Sigma>",
- "\\<Upsilon>",
- "\\<Phi>",
- "\\<Psi>",
- "\\<Omega>"
+ "\<A>",
+ "\<B>",
+ "\<C>",
+ "\<D>",
+ "\<E>",
+ "\<F>",
+ "\<G>",
+ "\<H>",
+ "\<I>",
+ "\<J>",
+ "\<K>",
+ "\<L>",
+ "\<M>",
+ "\<N>",
+ "\<O>",
+ "\<P>",
+ "\<Q>",
+ "\<R>",
+ "\<S>",
+ "\<T>",
+ "\<U>",
+ "\<V>",
+ "\<W>",
+ "\<X>",
+ "\<Y>",
+ "\<Z>",
+ "\<a>",
+ "\<b>",
+ "\<c>",
+ "\<d>",
+ "\<e>",
+ "\<f>",
+ "\<g>",
+ "\<h>",
+ "\<i>",
+ "\<j>",
+ "\<k>",
+ "\<l>",
+ "\<m>",
+ "\<n>",
+ "\<o>",
+ "\<p>",
+ "\<q>",
+ "\<r>",
+ "\<s>",
+ "\<t>",
+ "\<u>",
+ "\<v>",
+ "\<w>",
+ "\<x>",
+ "\<y>",
+ "\<z>",
+ "\<AA>",
+ "\<BB>",
+ "\<CC>",
+ "\<DD>",
+ "\<EE>",
+ "\<FF>",
+ "\<GG>",
+ "\<HH>",
+ "\<II>",
+ "\<JJ>",
+ "\<KK>",
+ "\<LL>",
+ "\<MM>",
+ "\<NN>",
+ "\<OO>",
+ "\<PP>",
+ "\<QQ>",
+ "\<RR>",
+ "\<SS>",
+ "\<TT>",
+ "\<UU>",
+ "\<VV>",
+ "\<WW>",
+ "\<XX>",
+ "\<YY>",
+ "\<ZZ>",
+ "\<aa>",
+ "\<bb>",
+ "\<cc>",
+ "\<dd>",
+ "\<ee>",
+ "\<ff>",
+ "\<gg>",
+ "\<hh>",
+ "\<ii>",
+ "\<jj>",
+ "\<kk>",
+ "\<ll>",
+ "\<mm>",
+ "\<nn>",
+ "\<oo>",
+ "\<pp>",
+ "\<qq>",
+ "\<rr>",
+ "\<ss>",
+ "\<tt>",
+ "\<uu>",
+ "\<vv>",
+ "\<ww>",
+ "\<xx>",
+ "\<yy>",
+ "\<zz>",
+ "\<alpha>",
+ "\<beta>",
+ "\<gamma>",
+ "\<delta>",
+ "\<epsilon>",
+ "\<zeta>",
+ "\<eta>",
+ "\<theta>",
+ "\<iota>",
+ "\<kappa>",
+ (*"\<lambda>", sic!*)
+ "\<mu>",
+ "\<nu>",
+ "\<xi>",
+ "\<pi>",
+ "\<rho>",
+ "\<sigma>",
+ "\<tau>",
+ "\<upsilon>",
+ "\<phi>",
+ "\<chi>",
+ "\<psi>",
+ "\<omega>",
+ "\<Gamma>",
+ "\<Delta>",
+ "\<Theta>",
+ "\<Lambda>",
+ "\<Xi>",
+ "\<Pi>",
+ "\<Sigma>",
+ "\<Upsilon>",
+ "\<Phi>",
+ "\<Psi>",
+ "\<Omega>"
];
in
@@ -421,7 +421,7 @@
fun is_quasi s = kind s = Quasi;
fun is_blank s = kind s = Blank;
-val is_block_ctrl = member (op =) ["\\<^bsub>", "\\<^esub>", "\\<^bsup>", "\\<^esup>"];
+val is_block_ctrl = member (op =) ["\<^bsub>", "\<^esub>", "\<^bsup>", "\<^esup>"];
fun is_quasi_letter s = let val k = kind s in k = Letter orelse k = Quasi end;
fun is_letdig s = let val k = kind s in k = Letter orelse k = Digit orelse k = Quasi end;
@@ -531,7 +531,7 @@
(* bump string -- treat as base 26 or base 1 numbers *)
-fun symbolic_end (_ :: "\\<^sub>" :: _) = true
+fun symbolic_end (_ :: "\<^sub>" :: _) = true
| symbolic_end ("'" :: ss) = symbolic_end ss
| symbolic_end (s :: _) = raw_symbolic s
| symbolic_end [] = false;
@@ -561,8 +561,8 @@
fun sym_len s =
if not (is_printable s) then (0: int)
- else if String.isPrefix "\\<long" s then 2
- else if String.isPrefix "\\<Long" s then 2
+ else if String.isPrefix "\<long" s then 2
+ else if String.isPrefix "\<Long" s then 2
else 1;
fun sym_length ss = fold (fn s => fn n => sym_len s + n) ss 0;
--- a/src/Pure/General/symbol.scala Sun Mar 06 20:39:19 2016 +0100
+++ b/src/Pure/General/symbol.scala Mon Mar 07 08:14:18 2016 +0100
@@ -54,6 +54,12 @@
def is_ascii_identifier(s: String): Boolean =
s.length > 0 && is_ascii_letter(s(0)) && s.forall(is_ascii_letdig)
+ def ascii(c: Char): Symbol =
+ {
+ if (c > 127) error("Non-ASCII character: " + quote(c.toString))
+ else char_symbols(c.toInt)
+ }
+
/* symbol matching */
--- a/src/Pure/General/symbol_pos.ML Sun Mar 06 20:39:19 2016 +0100
+++ b/src/Pure/General/symbol_pos.ML Mon Mar 07 08:14:18 2016 +0100
@@ -201,9 +201,9 @@
^ quote (content syms) ^ Position.here (#1 (range syms)));
in
(case syms of
- ("\\<open>", _) :: rest =>
+ ("\<open>", _) :: rest =>
(case rev rest of
- ("\\<close>", _) :: rrest => rev rrest
+ ("\<close>", _) :: rrest => rev rrest
| _ => err ())
| _ => err ())
end;
@@ -279,7 +279,7 @@
val letter = Scan.one (symbol #> Symbol.is_letter);
val letdigs1 = Scan.many1 (symbol #> Symbol.is_letdig);
-val sub = Scan.one (symbol #> (fn s => s = "\\<^sub>"));
+val sub = Scan.one (symbol #> (fn s => s = "\<^sub>"));
in
--- a/src/Pure/Isar/parse.ML Sun Mar 06 20:39:19 2016 +0100
+++ b/src/Pure/Isar/parse.ML Mon Mar 07 08:14:18 2016 +0100
@@ -211,7 +211,7 @@
group (fn () => "reserved identifier " ^ quote x)
(RESET_VALUE (Scan.one (Token.ident_with (fn y => x = y)) >> Token.content_of));
-val dots = sym_ident :-- (fn "\\<dots>" => Scan.succeed () | _ => Scan.fail) >> #1;
+val dots = sym_ident :-- (fn "\<dots>" => Scan.succeed () | _ => Scan.fail) >> #1;
val minus = sym_ident :-- (fn "-" => Scan.succeed () | _ => Scan.fail) >> #1;
--- a/src/Pure/ML/ml_compiler0.ML Sun Mar 06 20:39:19 2016 +0100
+++ b/src/Pure/ML/ml_compiler0.ML Mon Mar 07 08:14:18 2016 +0100
@@ -31,13 +31,14 @@
if String.isSuffix "\n" s then String.substring (s, 0, size s - 1)
else s;
-fun ml_positions start_line name txt =
+fun ml_input start_line name txt =
let
fun positions line (#"@" :: #"{" :: #"h" :: #"e" :: #"r" :: #"e" :: #"}" :: cs) res =
let val s = "(Position.line_file_only " ^ Int.toString line ^ " \"" ^ name ^ "\")"
in positions line cs (s :: res) end
- | positions line (c :: cs) res =
- positions (if c = #"\n" then line + 1 else line) cs (str c :: res)
+ | positions line (#"\\" :: #"<" :: cs) res = positions line cs ("\\\\<" :: res)
+ | positions line (#"\n" :: cs) res = positions (line + 1) cs ("\n" :: res)
+ | positions line (c :: cs) res = positions line cs (str c :: res)
| positions _ [] res = rev res;
in String.concat (positions start_line (String.explode txt) []) end;
@@ -46,7 +47,7 @@
val _ = Secure.deny_ml ();
val current_line = Unsynchronized.ref line;
- val in_buffer = Unsynchronized.ref (String.explode (ml_positions line file text));
+ val in_buffer = Unsynchronized.ref (String.explode (ml_input line file text));
val out_buffer = Unsynchronized.ref ([]: string list);
fun output () = drop_newline (implode (rev (! out_buffer)));
--- a/src/Pure/ML/ml_syntax.ML Sun Mar 06 20:39:19 2016 +0100
+++ b/src/Pure/ML/ml_syntax.ML Mon Mar 07 08:14:18 2016 +0100
@@ -1,7 +1,7 @@
(* Title: Pure/ML/ml_syntax.ML
Author: Makarius
-Basic ML syntax operations.
+Concrete ML syntax for basic values.
*)
signature ML_SYNTAX =
@@ -59,20 +59,25 @@
fun print_option f NONE = "NONE"
| print_option f (SOME x) = "SOME (" ^ f x ^ ")";
+fun print_chr s =
+ if Symbol.is_char s then
+ (case ord s of
+ 34 => "\\\""
+ | 92 => "\\\\"
+ | 9 => "\\t"
+ | 10 => "\\n"
+ | 11 => "\\f"
+ | 13 => "\\r"
+ | c =>
+ if c < 32 then "\\^" ^ chr (c + 64)
+ else if c < 127 then s
+ else "\\" ^ string_of_int c)
+ else error ("Bad character: " ^ quote s);
+
fun print_char s =
- if not (Symbol.is_char s) then s
- else if s = "\"" then "\\\""
- else if s = "\\" then "\\\\"
- else if s = "\t" then "\\t"
- else if s = "\n" then "\\n"
- else if s = "\f" then "\\f"
- else if s = "\r" then "\\r"
- else
- let val c = ord s in
- if c < 32 then "\\^" ^ chr (c + ord "@")
- else if c < 127 then s
- else "\\" ^ string_of_int c
- end;
+ if Symbol.is_char s then print_chr s
+ else if Symbol.is_utf8 s then translate_string print_chr s
+ else s;
val print_string = quote o implode o map print_char o Symbol.explode;
val print_strings = print_list print_string;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/ml_syntax.scala Mon Mar 07 08:14:18 2016 +0100
@@ -0,0 +1,36 @@
+/* Title: Pure/ML/ml_syntax.scala
+ Author: Makarius
+
+Concrete ML syntax for basic values.
+*/
+
+package isabelle
+
+
+object ML_Syntax
+{
+ private def print_chr(c: Byte): String =
+ c match {
+ case 34 => "\\\""
+ case 92 => "\\\\"
+ case 9 => "\\t"
+ case 10 => "\\n"
+ case 12 => "\\f"
+ case 13 => "\\r"
+ case _ =>
+ if (c < 0) "\\" + Library.signed_string_of_int(256 + c)
+ else if (c < 32) new String(Array[Char](92, 94, (c + 64).toChar))
+ else if (c < 127) Symbol.ascii(c.toChar)
+ else "\\" + Library.signed_string_of_int(c)
+ }
+
+ def print_char(s: Symbol.Symbol): String =
+ if (s.startsWith("\\<")) s
+ else UTF8.bytes(s).iterator.map(print_chr(_)).mkString
+
+ def print_string(str: String): String =
+ quote(Symbol.iterator(str).map(print_char(_)).mkString)
+
+ def print_string_raw(str: String): String =
+ quote(UTF8.bytes(str).iterator.map(print_chr(_)).mkString)
+}
--- a/src/Pure/Syntax/lexicon.ML Sun Mar 06 20:39:19 2016 +0100
+++ b/src/Pure/Syntax/lexicon.ML Mon Mar 07 08:14:18 2016 +0100
@@ -304,7 +304,7 @@
fun idxname cs ds = (implode (rev cs), nat 0 ds);
fun chop_idx [] ds = idxname [] ds
- | chop_idx (cs as (_ :: "\\<^sub>" :: _)) ds = idxname cs ds
+ | chop_idx (cs as (_ :: "\<^sub>" :: _)) ds = idxname cs ds
| chop_idx (c :: cs) ds =
if Symbol.is_digit c then chop_idx cs (c :: ds)
else idxname (c :: cs) ds;
@@ -426,10 +426,10 @@
fun marker s = (prefix s, unprefix s);
-val (mark_class, unmark_class) = marker "\\<^class>";
-val (mark_type, unmark_type) = marker "\\<^type>";
-val (mark_const, unmark_const) = marker "\\<^const>";
-val (mark_fixed, unmark_fixed) = marker "\\<^fixed>";
+val (mark_class, unmark_class) = marker "\<^class>";
+val (mark_type, unmark_type) = marker "\<^type>";
+val (mark_const, unmark_const) = marker "\<^const>";
+val (mark_fixed, unmark_fixed) = marker "\<^fixed>";
fun unmark {case_class, case_type, case_const, case_fixed, case_default} s =
(case try unmark_class s of
--- a/src/Pure/Syntax/syntax_ext.ML Sun Mar 06 20:39:19 2016 +0100
+++ b/src/Pure/Syntax/syntax_ext.ML Mon Mar 07 08:14:18 2016 +0100
@@ -140,7 +140,7 @@
local
-val is_meta = member (op =) ["(", ")", "/", "_", "\\<index>"];
+val is_meta = member (op =) ["(", ")", "/", "_", "\<index>"];
val scan_delim_char =
$$ "'" |-- Scan.one ((not o Symbol.is_blank) andf Symbol.not_eof) ||
@@ -151,7 +151,7 @@
val scan_sym =
$$ "_" >> K (Argument ("", 0)) ||
- $$ "\\<index>" >> K index ||
+ $$ "\<index>" >> K index ||
$$ "(" |-- Scan.many Symbol.is_digit >> (Bg o read_int) ||
$$ ")" >> K En ||
$$ "/" -- $$ "/" >> K (Brk ~1) ||
@@ -168,7 +168,7 @@
fun unique_index xsymbs =
if length (filter is_index xsymbs) <= 1 then xsymbs
- else error "Duplicate index arguments (\\<index>)";
+ else error "Duplicate index arguments (\<index>)";
in
--- a/src/Pure/Syntax/syntax_phases.ML Sun Mar 06 20:39:19 2016 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML Mon Mar 07 08:14:18 2016 +0100
@@ -179,7 +179,7 @@
in [Ast.Constant (Lexicon.mark_type c)] end
| asts_of (Parser.Node ("_position", [Parser.Tip tok])) = asts_of_position "_constrain" tok
| asts_of (Parser.Node ("_position_sort", [Parser.Tip tok])) = asts_of_position "_ofsort" tok
- | asts_of (Parser.Node (a as "\\<^const>Pure.dummy_pattern", [Parser.Tip tok])) =
+ | asts_of (Parser.Node (a as "\<^const>Pure.dummy_pattern", [Parser.Tip tok])) =
[ast_of_dummy a tok]
| asts_of (Parser.Node (a as "_idtdummy", [Parser.Tip tok])) =
[ast_of_dummy a tok]
@@ -797,7 +797,7 @@
(* type propositions *)
-fun type_prop_tr' ctxt T [Const ("\\<^const>Pure.sort_constraint", _)] =
+fun type_prop_tr' ctxt T [Const ("\<^const>Pure.sort_constraint", _)] =
Syntax.const "_sort_constraint" $ term_of_typ (Config.put show_sorts true ctxt) T
| type_prop_tr' ctxt T [t] =
Syntax.const "_ofclass" $ term_of_typ ctxt T $ t
@@ -839,7 +839,7 @@
("_context_xconst", const_ast_tr false)] #>
Sign.typed_print_translation
[("_type_prop", type_prop_tr'),
- ("\\<^const>Pure.type", type_tr'),
+ ("\<^const>Pure.type", type_tr'),
("_type_constraint_", type_constraint_tr')]);
--- a/src/Pure/Syntax/syntax_trans.ML Sun Mar 06 20:39:19 2016 +0100
+++ b/src/Pure/Syntax/syntax_trans.ML Mon Mar 07 08:14:18 2016 +0100
@@ -102,7 +102,7 @@
fun tappl_ast_tr [ty, tys, c] = Ast.mk_appl c (ty :: Ast.unfold_ast "_types" tys)
| tappl_ast_tr asts = raise Ast.AST ("tappl_ast_tr", asts);
-fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
+fun bracket_ast_tr [dom, cod] = Ast.fold_ast_p "\<^type>fun" (Ast.unfold_ast "_types" dom, cod)
| bracket_ast_tr asts = raise Ast.AST ("bracket_ast_tr", asts);
@@ -152,18 +152,18 @@
fun mk_type ty =
Syntax.const "_constrain" $
- Syntax.const "\\<^const>Pure.type" $ (Syntax.const "\\<^type>itself" $ ty);
+ Syntax.const "\<^const>Pure.type" $ (Syntax.const "\<^type>itself" $ ty);
fun ofclass_tr [ty, cls] = cls $ mk_type ty
| ofclass_tr ts = raise TERM ("ofclass_tr", ts);
-fun sort_constraint_tr [ty] = Syntax.const "\\<^const>Pure.sort_constraint" $ mk_type ty
+fun sort_constraint_tr [ty] = Syntax.const "\<^const>Pure.sort_constraint" $ mk_type ty
| sort_constraint_tr ts = raise TERM ("sort_constraint_tr", ts);
(* meta propositions *)
-fun aprop_tr [t] = Syntax.const "_constrain" $ t $ Syntax.const "\\<^type>prop"
+fun aprop_tr [t] = Syntax.const "_constrain" $ t $ Syntax.const "\<^type>prop"
| aprop_tr ts = raise TERM ("aprop_tr", ts);
@@ -174,7 +174,7 @@
(case Ast.unfold_ast_p "_asms" asms of
(asms', Ast.Appl [Ast.Constant "_asm", asm']) => asms' @ [asm']
| _ => raise Ast.AST ("bigimpl_ast_tr", asts))
- in Ast.fold_ast_p "\\<^const>Pure.imp" (prems, concl) end
+ in Ast.fold_ast_p "\<^const>Pure.imp" (prems, concl) end
| bigimpl_ast_tr asts = raise Ast.AST ("bigimpl_ast_tr", asts);
@@ -273,7 +273,7 @@
fun fun_ast_tr' asts =
if no_brackets () orelse no_type_brackets () then raise Match
else
- (case Ast.unfold_ast_p "\\<^type>fun" (Ast.Appl (Ast.Constant "\\<^type>fun" :: asts)) of
+ (case Ast.unfold_ast_p "\<^type>fun" (Ast.Appl (Ast.Constant "\<^type>fun" :: asts)) of
(dom as _ :: _ :: _, cod)
=> Ast.Appl [Ast.Constant "_bracket", Ast.fold_ast "_types" dom, cod]
| _ => raise Match);
@@ -389,8 +389,8 @@
fun impl_ast_tr' asts =
if no_brackets () then raise Match
else
- (case Ast.unfold_ast_p "\\<^const>Pure.imp"
- (Ast.Appl (Ast.Constant "\\<^const>Pure.imp" :: asts)) of
+ (case Ast.unfold_ast_p "\<^const>Pure.imp"
+ (Ast.Appl (Ast.Constant "\<^const>Pure.imp" :: asts)) of
(prems as _ :: _ :: _, concl) =>
let
val (asms, asm) = split_last prems;
@@ -501,11 +501,11 @@
("_struct", struct_tr)];
val pure_print_ast_translation =
- [("\\<^type>fun", fn _ => fun_ast_tr'),
+ [("\<^type>fun", fn _ => fun_ast_tr'),
("_abs", fn _ => abs_ast_tr'),
("_idts", fn _ => idtyp_ast_tr' "_idts"),
("_pttrns", fn _ => idtyp_ast_tr' "_pttrns"),
- ("\\<^const>Pure.imp", fn _ => impl_ast_tr'),
+ ("\<^const>Pure.imp", fn _ => impl_ast_tr'),
("_index", fn _ => index_ast_tr'),
("_struct", struct_ast_tr')];
--- a/src/Pure/System/utf8.scala Sun Mar 06 20:39:19 2016 +0100
+++ b/src/Pure/System/utf8.scala Mon Mar 07 08:14:18 2016 +0100
@@ -20,6 +20,8 @@
val charset: Charset = Charset.forName(charset_name)
def codec(): Codec = Codec(charset)
+ def bytes(s: String): Array[Byte] = s.getBytes(charset)
+
/* permissive UTF-8 decoding */
--- a/src/Pure/Thy/html.ML Sun Mar 06 20:39:19 2016 +0100
+++ b/src/Pure/Thy/html.ML Mon Mar 07 08:14:18 2016 +0100
@@ -39,10 +39,10 @@
val mapping =
map (apsnd (fn c => "&#" ^ Markup.print_int c ^ ";")) codes @
[("'", "'"),
- ("\\<^bsub>", hidden "⇘" ^ "<sub>"),
- ("\\<^esub>", hidden "⇙" ^ "</sub>"),
- ("\\<^bsup>", hidden "⇗" ^ "<sup>"),
- ("\\<^esup>", hidden "⇖" ^ "</sup>")];
+ ("\<^bsub>", hidden "⇘" ^ "<sub>"),
+ ("\<^esub>", hidden "⇙" ^ "</sub>"),
+ ("\<^bsup>", hidden "⇗" ^ "<sup>"),
+ ("\<^esup>", hidden "⇖" ^ "</sup>")];
in Symbols (fold Symtab.update mapping Symtab.empty) end;
val no_symbols = make_symbols [];
@@ -70,9 +70,9 @@
let
val (s2, ss) = (case rest of [] => ("", []) | s2 :: ss => (s2, ss));
val (s, r) =
- if s1 = "\\<^sub>" then (output_sub symbols "⇩" s2, ss)
- else if s1 = "\\<^sup>" then (output_sup symbols "⇧" s2, ss)
- else if s1 = "\\<^bold>" then (output_bold symbols "❙" s2, ss)
+ if s1 = "\<^sub>" then (output_sub symbols "⇩" s2, ss)
+ else if s1 = "\<^sup>" then (output_sup symbols "⇧" s2, ss)
+ else if s1 = "\<^bold>" then (output_bold symbols "❙" s2, ss)
else (output_sym symbols s1, rest);
in output_syms symbols r (s :: result) end;
@@ -120,19 +120,19 @@
(* document *)
fun begin_document symbols title =
- "<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n\
- \<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" \
- \\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n\
- \<html xmlns=\"http://www.w3.org/1999/xhtml\">\n\
- \<head>\n\
- \<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n\
- \<title>" ^ output symbols (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n\
- \<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n\
- \</head>\n\
- \\n\
- \<body>\n\
- \<div class=\"head\">\
- \<h1>" ^ output symbols title ^ "</h1>\n";
+ "<?xml version=\"1.0\" encoding=\"utf-8\" ?>\n" ^
+ "<!DOCTYPE html PUBLIC \"-//W3C//DTD XHTML 1.0 Transitional//EN\" " ^
+ "\"http://www.w3.org/TR/xhtml1/DTD/xhtml1-transitional.dtd\">\n" ^
+ "<html xmlns=\"http://www.w3.org/1999/xhtml\">\n" ^
+ "<head>\n" ^
+ "<meta http-equiv=\"Content-Type\" content=\"text/html; charset=utf-8\"/>\n" ^
+ "<title>" ^ output symbols (title ^ " (" ^ Distribution.version ^ ")") ^ "</title>\n" ^
+ "<link media=\"all\" rel=\"stylesheet\" type=\"text/css\" href=\"isabelle.css\"/>\n" ^
+ "</head>\n" ^
+ "\n" ^
+ "<body>\n" ^
+ "<div class=\"head\">" ^
+ "<h1>" ^ output symbols title ^ "</h1>\n";
val end_document = "\n</div>\n</body>\n</html>\n";
--- a/src/Pure/Thy/markdown.ML Sun Mar 06 20:39:19 2016 +0100
+++ b/src/Pure/Thy/markdown.ML Mon Mar 07 08:14:18 2016 +0100
@@ -49,7 +49,7 @@
val kinds = [("item", Itemize), ("enum", Enumerate), ("descr", Description)];
-val is_control = member (op =) ["\\<^item>", "\\<^enum>", "\\<^descr>"];
+val is_control = member (op =) ["\<^item>", "\<^enum>", "\<^descr>"];
(* document lines *)
--- a/src/Pure/build-jars Sun Mar 06 20:39:19 2016 +0100
+++ b/src/Pure/build-jars Mon Mar 07 08:14:18 2016 +0100
@@ -55,6 +55,7 @@
Isar/parse.scala
Isar/token.scala
ML/ml_lex.scala
+ ML/ml_syntax.scala
PIDE/batch_session.scala
PIDE/command.scala
PIDE/command_span.scala
--- a/src/Pure/library.ML Sun Mar 06 20:39:19 2016 +0100
+++ b/src/Pure/library.ML Mon Mar 07 08:14:18 2016 +0100
@@ -693,7 +693,7 @@
(*simple quoting (does not escape special chars)*)
val quote = enclose "\"" "\"";
-val cartouche = enclose "\\<open>" "\\<close>";
+val cartouche = enclose "\<open>" "\<close>";
val space_implode = String.concatWith;
--- a/src/Pure/pure_thy.ML Sun Mar 06 20:39:19 2016 +0100
+++ b/src/Pure/pure_thy.ML Mon Mar 07 08:14:18 2016 +0100
@@ -108,12 +108,12 @@
("_tappl", typ "type => types => type_name => type", Delimfix "((1'(_,/ _')) _)"),
("", typ "type => types", Delimfix "_"),
("_types", typ "type => types => types", Delimfix "_,/ _"),
- ("\\<^type>fun", typ "type => type => type", Mixfix ("(_/ \\<Rightarrow> _)", [1, 0], 0)),
- ("_bracket", typ "types => type => type", Mixfix ("([_]/ \\<Rightarrow> _)", [0, 0], 0)),
+ ("\<^type>fun", typ "type => type => type", Mixfix ("(_/ \<Rightarrow> _)", [1, 0], 0)),
+ ("_bracket", typ "types => type => type", Mixfix ("([_]/ \<Rightarrow> _)", [0, 0], 0)),
("", typ "type => type", Delimfix "'(_')"),
- ("\\<^type>dummy", typ "type", Delimfix "'_"),
+ ("\<^type>dummy", typ "type", Delimfix "'_"),
("_type_prop", typ "'a", NoSyn),
- ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\\<lambda>_./ _)", [0, 3], 3)),
+ ("_lambda", typ "pttrns => 'a => logic", Mixfix ("(3\<lambda>_./ _)", [0, 3], 3)),
("_abs", typ "'a", NoSyn),
("", typ "'a => args", Delimfix "_"),
("_args", typ "'a => args => args", Delimfix "_,/ _"),
@@ -131,26 +131,26 @@
("", typ "id_position => aprop", Delimfix "_"),
("", typ "longid_position => aprop", Delimfix "_"),
("", typ "var_position => aprop", Delimfix "_"),
- ("_DDDOT", typ "aprop", Delimfix "\\<dots>"),
+ ("_DDDOT", typ "aprop", Delimfix "\<dots>"),
("_aprop", typ "aprop => prop", Delimfix "PROP _"),
("_asm", typ "prop => asms", Delimfix "_"),
("_asms", typ "prop => asms => asms", Delimfix "_;/ _"),
- ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\\<lbrakk>_\\<rbrakk>)/ \\<Longrightarrow> _)", [0, 1], 1)),
+ ("_bigimpl", typ "asms => prop => prop", Mixfix ("((1\<lbrakk>_\<rbrakk>)/ \<Longrightarrow> _)", [0, 1], 1)),
("_ofclass", typ "type => logic => prop", Delimfix "(1OFCLASS/(1'(_,/ _')))"),
("_mk_ofclass", typ "dummy", NoSyn),
("_TYPE", typ "type => logic", Delimfix "(1TYPE/(1'(_')))"),
("", typ "id_position => logic", Delimfix "_"),
("", typ "longid_position => logic", Delimfix "_"),
("", typ "var_position => logic", Delimfix "_"),
- ("_DDDOT", typ "logic", Delimfix "\\<dots>"),
+ ("_DDDOT", typ "logic", Delimfix "\<dots>"),
("_strip_positions", typ "'a", NoSyn),
("_position", typ "num_token => num_position", Delimfix "_"),
("_position", typ "float_token => float_position", Delimfix "_"),
("_constify", typ "num_position => num_const", Delimfix "_"),
("_constify", typ "float_position => float_const", Delimfix "_"),
- ("_index", typ "logic => index", Delimfix "(00\\<^bsub>_\\<^esub>)"),
+ ("_index", typ "logic => index", Delimfix "(00\<^bsub>_\<^esub>)"),
("_indexdefault", typ "index", Delimfix ""),
- ("_indexvar", typ "index", Delimfix "'\\<index>"),
+ ("_indexvar", typ "index", Delimfix "'\<index>"),
("_struct", typ "index => logic", NoSyn),
("_update_name", typ "idt", NoSyn),
("_constrainAbs", typ "'a", NoSyn),
@@ -189,9 +189,9 @@
#> Sign.add_syntax ("", false)
[(const "Pure.prop", typ "prop => prop", Mixfix ("_", [0], 0))]
#> Sign.add_consts
- [(qualify (Binding.make ("eq", @{here})), typ "'a => 'a => prop", Infix ("\\<equiv>", 2)),
- (qualify (Binding.make ("imp", @{here})), typ "prop => prop => prop", Infixr ("\\<Longrightarrow>", 1)),
- (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", Binder ("\\<And>", 0, 0)),
+ [(qualify (Binding.make ("eq", @{here})), typ "'a => 'a => prop", Infix ("\<equiv>", 2)),
+ (qualify (Binding.make ("imp", @{here})), typ "prop => prop => prop", Infixr ("\<Longrightarrow>", 1)),
+ (qualify (Binding.make ("all", @{here})), typ "('a => prop) => prop", Binder ("\<And>", 0, 0)),
(qualify (Binding.make ("prop", @{here})), typ "prop => prop", NoSyn),
(qualify (Binding.make ("type", @{here})), typ "'a itself", NoSyn),
(qualify (Binding.make ("dummy_pattern", @{here})), typ "'a", Delimfix "'_")]
--- a/src/Pure/term.ML Sun Mar 06 20:39:19 2016 +0100
+++ b/src/Pure/term.ML Mon Mar 07 08:14:18 2016 +0100
@@ -986,7 +986,7 @@
val idx = string_of_int i;
val dot =
(case rev (Symbol.explode x) of
- _ :: "\\<^sub>" :: _ => false
+ _ :: "\<^sub>" :: _ => false
| c :: _ => Symbol.is_digit c
| _ => true);
in
--- a/src/Tools/jEdit/src/isabelle_encoding.scala Sun Mar 06 20:39:19 2016 +0100
+++ b/src/Tools/jEdit/src/isabelle_encoding.scala Mon Mar 07 08:14:18 2016 +0100
@@ -56,7 +56,7 @@
override def flush()
{
val text = Symbol.encode(toString(UTF8.charset_name))
- out.write(text.getBytes(UTF8.charset))
+ out.write(UTF8.bytes(text))
out.flush()
}
override def close() { out.close() }