# HG changeset patch # User paulson # Date 1474556197 -3600 # Node ID d4b89572ae718d1e6e112a619169321fa4a2bf4f # Parent f6ce08859d4c015a71dae3e5ba4e59f629960d27# Parent 45ed7d0aeb6fdc5d46858506b04e23876a34cd58 Merge diff -r f6ce08859d4c -r d4b89572ae71 NEWS --- a/NEWS Thu Sep 22 15:44:47 2016 +0100 +++ b/NEWS Thu Sep 22 15:56:37 2016 +0100 @@ -30,6 +30,15 @@ to "(\indent=DIGITS\". The former notation "(00" for unbreakable blocks is superseded by "(\unbreabable\" --- rare INCOMPATIBILITY. +* Mixfix annotations support delimiters like \<^control>\cartouche\ -- +this allows special forms of document output. + +* Raw LaTeX output now works via \<^latex>\...\ instead of raw control +symbol \<^raw:...>. INCOMPATIBILITY, notably for LaTeXsugar.thy and its +derivatives. + +* \<^raw:...> symbols are no longer supported. + * New symbol \, e.g. for temporal operator. * Old 'header' command is no longer supported (legacy since diff -r f6ce08859d4c -r d4b89572ae71 src/Doc/Implementation/ML.thy --- a/src/Doc/Implementation/ML.thy Thu Sep 22 15:44:47 2016 +0100 +++ b/src/Doc/Implementation/ML.thy Thu Sep 22 15:56:37 2016 +0100 @@ -1217,13 +1217,6 @@ \<^enum> a control symbol ``\<^verbatim>\\<^ident>\'', for example ``\<^verbatim>\\<^bold>\'', - \<^enum> a raw symbol ``\<^verbatim>\\\\<^verbatim>\<^raw:\\text\\<^verbatim>\>\'' where \text\ consists of - printable characters excluding ``\<^verbatim>\.\'' and ``\<^verbatim>\>\'', for example - ``\<^verbatim>\\<^raw:$\sum_{i = 1}^n$>\'', - - \<^enum> a numbered raw control symbol ``\<^verbatim>\\\\<^verbatim>\<^raw\\n\\<^verbatim>\>\, where \n\ consists - of digits, for example ``\<^verbatim>\\<^raw42>\''. - The \ident\ syntax for symbol names is \letter (letter | digit)\<^sup>*\, where \letter = A..Za..z\ and \digit = 0..9\. There are infinitely many regular symbols and control symbols, but a fixed collection of standard symbols is @@ -1275,7 +1268,7 @@ \<^descr> Type @{ML_type "Symbol.sym"} is a concrete datatype that represents the different kinds of symbols explicitly, with constructors @{ML "Symbol.Char"}, @{ML "Symbol.UTF8"}, @{ML "Symbol.Sym"}, @{ML - "Symbol.Control"}, @{ML "Symbol.Raw"}, @{ML "Symbol.Malformed"}. + "Symbol.Control"}, @{ML "Symbol.Malformed"}. \<^descr> @{ML "Symbol.decode"} converts the string representation of a symbol into the datatype version. diff -r f6ce08859d4c -r d4b89572ae71 src/Doc/Isar_Ref/Inner_Syntax.thy --- a/src/Doc/Isar_Ref/Inner_Syntax.thy Thu Sep 22 15:44:47 2016 +0100 +++ b/src/Doc/Isar_Ref/Inner_Syntax.thy Thu Sep 22 15:56:37 2016 +0100 @@ -329,20 +329,21 @@ printing, notably spaces, blocks, and breaks. The general template format is a sequence over any of the following entities. - \<^descr> \d\ is a delimiter, namely a non-empty sequence of characters other than - the following special characters: - - \<^medskip> - \begin{tabular}{ll} - \<^verbatim>\'\ & single quote \\ - \<^verbatim>\_\ & underscore \\ - \\\ & index symbol \\ - \<^verbatim>\(\ & open parenthesis \\ - \<^verbatim>\)\ & close parenthesis \\ - \<^verbatim>\/\ & slash \\ - \\ \\ & cartouche delimiters \\ - \end{tabular} - \<^medskip> + \<^descr> \d\ is a delimiter, namely a non-empty sequence delimiter items of the + following form: + \<^enum> a control symbol followed by a cartouche + \<^enum> a single symbol, excluding the following special characters: + \<^medskip> + \begin{tabular}{ll} + \<^verbatim>\'\ & single quote \\ + \<^verbatim>\_\ & underscore \\ + \\\ & index symbol \\ + \<^verbatim>\(\ & open parenthesis \\ + \<^verbatim>\)\ & close parenthesis \\ + \<^verbatim>\/\ & slash \\ + \\ \\ & cartouche delimiters \\ + \end{tabular} + \<^medskip> \<^descr> \<^verbatim>\'\ escapes the special meaning of these meta-characters, producing a literal version of the following character, unless that is a blank. diff -r f6ce08859d4c -r d4b89572ae71 src/Doc/Main/Main_Doc.thy --- a/src/Doc/Main/Main_Doc.thy Thu Sep 22 15:44:47 2016 +0100 +++ b/src/Doc/Main/Main_Doc.thy Thu Sep 22 15:56:37 2016 +0100 @@ -229,7 +229,7 @@ \begin{tabular}{@ {} l @ {\quad$\equiv$\quad} ll @ {}} @{term "Pair a b"} & @{term[source]"Pair a b"}\\ @{term "case_prod (\x y. t)"} & @{term[source]"case_prod (\x y. t)"}\\ -@{term "A \ B"} & \Sigma A (\\<^raw:\_>. B)\ +@{term "A \ B"} & \Sigma A (\\<^latex>\\_\. B)\ \end{tabular} Pairs may be nested. Nesting to the right is printed as a tuple, diff -r f6ce08859d4c -r d4b89572ae71 src/Doc/Prog_Prove/Bool_nat_list.thy --- a/src/Doc/Prog_Prove/Bool_nat_list.thy Thu Sep 22 15:44:47 2016 +0100 +++ b/src/Doc/Prog_Prove/Bool_nat_list.thy Thu Sep 22 15:56:37 2016 +0100 @@ -69,7 +69,7 @@ Because both subgoals are easy, Isabelle can do it. The base case @{prop"add 0 0 = 0"} holds by definition of @{const add}, and the induction step is almost as simple: -@{text"add\<^raw:~>(Suc m) 0 = Suc(add m 0) = Suc m"} +@{text"add\<^latex>\~\(Suc m) 0 = Suc(add m 0) = Suc m"} using first the definition of @{const add} and then the induction hypothesis. In summary, both subproofs rely on simplification with function definitions and the induction hypothesis. diff -r f6ce08859d4c -r d4b89572ae71 src/Doc/Prog_Prove/LaTeXsugar.thy --- a/src/Doc/Prog_Prove/LaTeXsugar.thy Thu Sep 22 15:44:47 2016 +0100 +++ b/src/Doc/Prog_Prove/LaTeXsugar.thy Thu Sep 22 15:56:37 2016 +0100 @@ -9,38 +9,38 @@ begin (* DUMMY *) -consts DUMMY :: 'a ("\<^raw:\_>") +consts DUMMY :: 'a ("\<^latex>\\\_\") (* THEOREMS *) notation (Rule output) - Pure.imp ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>") + Pure.imp ("\<^latex>\\\mbox{}\\inferrule{\\mbox{\_\<^latex>\}}\\<^latex>\{\\mbox{\_\<^latex>\}}\") syntax (Rule output) "_bigimpl" :: "asms \ prop \ prop" - ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>") + ("\<^latex>\\\mbox{}\\inferrule{\_\<^latex>\}\\<^latex>\{\\mbox{\_\<^latex>\}}\") "_asms" :: "prop \ asms \ asms" - ("\<^raw:\mbox{>_\<^raw:}\\>/ _") + ("\<^latex>\\\mbox{\_\<^latex>\}\\\\\/ _") - "_asm" :: "prop \ asms" ("\<^raw:\mbox{>_\<^raw:}>") + "_asm" :: "prop \ asms" ("\<^latex>\\\mbox{\_\<^latex>\}\") notation (Axiom output) - "Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>") + "Trueprop" ("\<^latex>\\\mbox{}\\inferrule{\\mbox{}}{\\mbox{\_\<^latex>\}}\") notation (IfThen output) - Pure.imp ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") + Pure.imp ("\<^latex>\{\\normalsize{}\If\<^latex>\\\,}\ _/ \<^latex>\{\\normalsize \\,\then\<^latex>\\\,}\/ _.") syntax (IfThen output) "_bigimpl" :: "asms \ prop \ prop" - ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") - "_asms" :: "prop \ asms \ asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") - "_asm" :: "prop \ asms" ("\<^raw:\mbox{>_\<^raw:}>") + ("\<^latex>\{\\normalsize{}\If\<^latex>\\\,}\ _ /\<^latex>\{\\normalsize \\,\then\<^latex>\\\,}\/ _.") + "_asms" :: "prop \ asms \ asms" ("\<^latex>\\\mbox{\_\<^latex>\}\ /\<^latex>\{\\normalsize \\,\and\<^latex>\\\,}\/ _") + "_asm" :: "prop \ asms" ("\<^latex>\\\mbox{\_\<^latex>\}\") notation (IfThenNoBox output) - Pure.imp ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") + Pure.imp ("\<^latex>\{\\normalsize{}\If\<^latex>\\\,}\ _/ \<^latex>\{\\normalsize \\,\then\<^latex>\\\,}\/ _.") syntax (IfThenNoBox output) "_bigimpl" :: "asms \ prop \ prop" - ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") - "_asms" :: "prop \ asms \ asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") + ("\<^latex>\{\\normalsize{}\If\<^latex>\\\,}\ _ /\<^latex>\{\\normalsize \\,\then\<^latex>\\\,}\/ _.") + "_asms" :: "prop \ asms \ asms" ("_ /\<^latex>\{\\normalsize \\,\and\<^latex>\\\,}\/ _") "_asm" :: "prop \ asms" ("_") setup{* diff -r f6ce08859d4c -r d4b89572ae71 src/Doc/Prog_Prove/Logic.thy --- a/src/Doc/Prog_Prove/Logic.thy Thu Sep 22 15:44:47 2016 +0100 +++ b/src/Doc/Prog_Prove/Logic.thy Thu Sep 22 15:56:37 2016 +0100 @@ -340,7 +340,7 @@ The expression @{text"conjI[of \"a=b\" \"False\"]"} instantiates the unknowns in @{thm[source] conjI} from left to right with the two formulas @{text"a=b"} and @{text False}, yielding the rule -@{thm[display,mode=Rule]conjI[of "a=b" False]} +@{thm[display,mode=Rule,margin=100]conjI[of "a=b" False]} In general, @{text"th[of string\<^sub>1 \ string\<^sub>n]"} instantiates the unknowns in the theorem @{text th} from left to right with the terms diff -r f6ce08859d4c -r d4b89572ae71 src/HOL/Decision_Procs/Approximation.thy --- a/src/HOL/Decision_Procs/Approximation.thy Thu Sep 22 15:44:47 2016 +0100 +++ b/src/HOL/Decision_Procs/Approximation.thy Thu Sep 22 15:56:37 2016 +0100 @@ -2863,29 +2863,6 @@ interpret_floatarith_divide interpret_floatarith_diff by auto -lemma interpret_floatarith_tan: - "interpret_floatarith (Mult (Cos (Add (Mult Pi (Num (Float 1 (- 1)))) (Minus a))) (Inverse (Cos a))) vs = - tan (interpret_floatarith a vs)" - unfolding interpret_floatarith.simps(3,4) interpret_floatarith_sin tan_def divide_inverse - by auto - -lemma interpret_floatarith_log: - "interpret_floatarith ((Mult (Ln x) (Inverse (Ln b)))) vs = - log (interpret_floatarith b vs) (interpret_floatarith x vs)" - unfolding log_def interpret_floatarith.simps divide_inverse .. - -lemma interpret_floatarith_num: - shows "interpret_floatarith (Num (Float 0 0)) vs = 0" - and "interpret_floatarith (Num (Float 1 0)) vs = 1" - and "interpret_floatarith (Num (Float (- 1) 0)) vs = - 1" - and "interpret_floatarith (Num (Float (numeral a) 0)) vs = numeral a" - and "interpret_floatarith (Num (Float (- numeral a) 0)) vs = - numeral a" - by auto - -lemma interpret_floatarith_ceiling: - "interpret_floatarith (Minus (Floor (Minus a))) vs = ceiling (interpret_floatarith a vs)" - unfolding ceiling_def interpret_floatarith.simps of_int_minus .. - subsection "Implement approximation function" @@ -4289,10 +4266,6 @@ subsection \Implement proof method \texttt{approximation}\ -lemmas interpret_form_equations = interpret_form.simps interpret_floatarith.simps interpret_floatarith_num - interpret_floatarith_divide interpret_floatarith_diff interpret_floatarith_tan interpret_floatarith_log - interpret_floatarith_sin interpret_floatarith_ceiling - oracle approximation_oracle = \fn (thy, t) => let fun bad t = error ("Bad term: " ^ Syntax.string_of_term_global thy t); @@ -4400,6 +4373,61 @@ lemma meta_eqE: "x \ a \ \ x = a \ P\ \ P" by auto +named_theorems approximation_preproc + +lemma approximation_preproc_floatarith[approximation_preproc]: + "0 = real_of_float 0" + "1 = real_of_float 1" + "0 = Float 0 0" + "1 = Float 1 0" + "numeral a = Float (numeral a) 0" + "numeral a = real_of_float (numeral a)" + "x - y = x + - y" + "x / y = x * inverse y" + "ceiling x = - floor (- x)" + "log x y = ln y * inverse (ln x)" + "sin x = cos (pi / 2 - x)" + "tan x = sin x / cos x" + by (simp_all add: inverse_eq_divide ceiling_def log_def sin_cos_eq tan_def real_of_float_eq) + +lemma approximation_preproc_int[approximation_preproc]: + "real_of_int 0 = real_of_float 0" + "real_of_int 1 = real_of_float 1" + "real_of_int (i + j) = real_of_int i + real_of_int j" + "real_of_int (- i) = - real_of_int i" + "real_of_int (i - j) = real_of_int i - real_of_int j" + "real_of_int (i * j) = real_of_int i * real_of_int j" + "real_of_int (i div j) = real_of_int (floor (real_of_int i / real_of_int j))" + "real_of_int (min i j) = min (real_of_int i) (real_of_int j)" + "real_of_int (max i j) = max (real_of_int i) (real_of_int j)" + "real_of_int (abs i) = abs (real_of_int i)" + "real_of_int (i ^ n) = (real_of_int i) ^ n" + "real_of_int (numeral a) = real_of_float (numeral a)" + "i mod j = i - i div j * j" + "i = j \ real_of_int i = real_of_int j" + "i \ j \ real_of_int i \ real_of_int j" + "i < j \ real_of_int i < real_of_int j" + "i \ {j .. k} \ real_of_int i \ {real_of_int j .. real_of_int k}" + by (simp_all add: floor_divide_of_int_eq zmod_zdiv_equality') + +lemma approximation_preproc_nat[approximation_preproc]: + "real 0 = real_of_float 0" + "real 1 = real_of_float 1" + "real (i + j) = real i + real j" + "real (i - j) = max (real i - real j) 0" + "real (i * j) = real i * real j" + "real (i div j) = real_of_int (floor (real i / real j))" + "real (min i j) = min (real i) (real j)" + "real (max i j) = max (real i) (real j)" + "real (i ^ n) = (real i) ^ n" + "real (numeral a) = real_of_float (numeral a)" + "i mod j = i - i div j * j" + "n = m \ real n = real m" + "n \ m \ real n \ real m" + "n < m \ real n < real m" + "n \ {m .. l} \ real n \ {real m .. real l}" + by (simp_all add: real_div_nat_eq_floor_of_divide mod_div_equality') + ML_file "approximation.ML" method_setup approximation = \ @@ -4421,6 +4449,17 @@ section "Quickcheck Generator" +lemma approximation_preproc_push_neg[approximation_preproc]: + fixes a b::real + shows + "\ (a < b) \ b \ a" + "\ (a \ b) \ b < a" + "\ (a = b) \ b < a \ a < b" + "\ (p \ q) \ \ p \ \ q" + "\ (p \ q) \ \ p \ \ q" + "\ \ q \ q" + by auto + ML_file "approximation_generator.ML" setup "Approximation_Generator.setup" diff -r f6ce08859d4c -r d4b89572ae71 src/HOL/Decision_Procs/approximation.ML --- a/src/HOL/Decision_Procs/approximation.ML Thu Sep 22 15:44:47 2016 +0100 +++ b/src/HOL/Decision_Procs/approximation.ML Thu Sep 22 15:56:37 2016 +0100 @@ -4,6 +4,7 @@ signature APPROXIMATION = sig + val reify_form: Proof.context -> term -> term val approx: int -> Proof.context -> term -> term val approximate: Proof.context -> term -> term val approximation_tac : int -> (string * int) list -> int option -> Proof.context -> int -> tactic @@ -54,13 +55,12 @@ (Object_Logic.judgment_conv ctxt (Conv.params_conv (~1) (K (Conv.concl_conv (~1) conv)) ctxt)) THEN' resolve_tac ctxt [TrueI] -val form_equations = @{thms interpret_form_equations}; - fun rewrite_interpret_form_tac ctxt prec splitting taylor i st = let - fun lookup_splitting (Free (name, _)) - = case AList.lookup (op =) splitting name - of SOME s => HOLogic.mk_number @{typ nat} s - | NONE => @{term "0 :: nat"} + fun lookup_splitting (Free (name, _)) = + (case AList.lookup (op =) splitting name + of SOME s => HOLogic.mk_number @{typ nat} s + | NONE => @{term "0 :: nat"}) + | lookup_splitting t = raise TERM ("lookup_splitting", [t]) val vs = nth (Thm.prems_of st) (i - 1) |> Logic.strip_imp_concl |> HOLogic.dest_Trueprop @@ -117,9 +117,13 @@ fun dest_interpret (@{const "interpret_floatarith"} $ b $ xs) = (b, xs) | dest_interpret t = raise TERM ("dest_interpret", [t]) +fun dest_interpret_env (@{const "interpret_form"} $ _ $ xs) = xs + | dest_interpret_env (@{const "interpret_floatarith"} $ _ $ xs) = xs + | dest_interpret_env t = raise TERM ("dest_interpret_env", [t]) -fun dest_float (@{const "Float"} $ m $ e) = - (snd (HOLogic.dest_number m), snd (HOLogic.dest_number e)) +fun dest_float (@{const "Float"} $ m $ e) = (snd (HOLogic.dest_number m), snd (HOLogic.dest_number e)) + | dest_float t = raise TERM ("dest_float", [t]) + fun dest_ivl (Const (@{const_name "Some"}, _) $ (Const (@{const_name Pair}, _) $ u $ l)) = SOME (dest_float u, dest_float l) @@ -138,8 +142,8 @@ let val (m, e) = (if e < 0 then (m,e) else (m * Integer.pow e 2, 0)) - fun frac c p 0 digits cnt = (digits, cnt, 0) - | frac c 0 r digits cnt = (digits, cnt, r) + fun frac _ _ 0 digits cnt = (digits, cnt, 0) + | frac _ 0 r digits cnt = (digits, cnt, r) | frac c p r digits cnt = (let val (d, r) = Integer.div_mod (r * 10) (Integer.pow (~e) 2) in frac (c orelse d <> 0) (if d <> 0 orelse c then p - 1 else p) r @@ -190,21 +194,52 @@ |> SINGLE tactic |> the |> Thm.prems_of |> hd -fun prepare_form ctxt term = apply_tactic ctxt term ( - REPEAT (FIRST' [eresolve_tac ctxt @{thms intervalE}, - eresolve_tac ctxt @{thms meta_eqE}, - resolve_tac ctxt @{thms impI}] 1) - THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} => reorder_bounds_tac ctxt' prems 1) ctxt 1 - THEN DETERM (TRY (filter_prems_tac ctxt (K false) 1))) +fun preproc_form_conv ctxt = + Simplifier.rewrite + (put_simpset HOL_basic_ss ctxt addsimps + (Named_Theorems.get ctxt @{named_theorems approximation_preproc})) + +fun reify_form_conv ctxt ct = + let + val thm = + Reification.conv ctxt @{thms interpret_form.simps interpret_floatarith.simps} ct + handle ERROR msg => + cat_error ("Reification failed: " ^ msg) + ("Approximation does not support " ^ + quote (Syntax.string_of_term ctxt (Thm.term_of ct))) + fun check_env (Free _) = () + | check_env (Var _) = () + | check_env t = + cat_error "Term not supported by approximation:" (Syntax.string_of_term ctxt t) + val _ = Thm.rhs_of thm |> Thm.term_of |> dest_interpret_env |> HOLogic.dest_list |> map check_env + in thm end -fun reify_form ctxt term = apply_tactic ctxt term - (Reification.tac ctxt form_equations NONE 1) + +fun reify_form_tac ctxt i = CONVERSION (Conv.arg_conv (reify_form_conv ctxt)) i + +fun prepare_form_tac ctxt i = + REPEAT (FIRST' [eresolve_tac ctxt @{thms intervalE}, + eresolve_tac ctxt @{thms meta_eqE}, + resolve_tac ctxt @{thms impI}] i) + THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} => reorder_bounds_tac ctxt' prems i) ctxt i + THEN DETERM (TRY (filter_prems_tac ctxt (K false) i)) + THEN CONVERSION (Conv.arg_conv (preproc_form_conv ctxt)) i + +fun prepare_form ctxt term = apply_tactic ctxt term (prepare_form_tac ctxt 1) + +fun apply_reify_form ctxt t = apply_tactic ctxt t (reify_form_tac ctxt 1) + +fun reify_form ctxt t = HOLogic.mk_Trueprop t + |> prepare_form ctxt + |> apply_reify_form ctxt + |> HOLogic.dest_Trueprop fun approx_form prec ctxt t = realify t |> prepare_form ctxt - |> (fn arith_term => reify_form ctxt arith_term - |> HOLogic.dest_Trueprop |> dest_interpret_form + |> (fn arith_term => apply_reify_form ctxt arith_term + |> HOLogic.dest_Trueprop + |> dest_interpret_form |> (fn (data, xs) => mk_approx_form_eval prec data (HOLogic.mk_list @{typ "(float * float) option"} (map (fn _ => @{term "None :: (float * float) option"}) (HOLogic.dest_list xs))) @@ -216,7 +251,7 @@ fun approx_arith prec ctxt t = realify t |> Thm.cterm_of ctxt - |> Reification.conv ctxt form_equations + |> (preproc_form_conv ctxt then_conv reify_form_conv ctxt) |> Thm.prop_of |> Logic.dest_equals |> snd |> dest_interpret |> fst @@ -252,13 +287,9 @@ >> (fn (modes, t) => Toplevel.keep (approximate_cmd modes t))); fun approximation_tac prec splitting taylor ctxt i = - REPEAT (FIRST' [eresolve_tac ctxt @{thms intervalE}, - eresolve_tac ctxt @{thms meta_eqE}, - resolve_tac ctxt @{thms impI}] i) - THEN Subgoal.FOCUS (fn {prems, context = ctxt', ...} => reorder_bounds_tac ctxt' prems i) ctxt i - THEN DETERM (TRY (filter_prems_tac ctxt (K false) i)) - THEN DETERM (Reification.tac ctxt form_equations NONE i) + prepare_form_tac ctxt i + THEN reify_form_tac ctxt i THEN rewrite_interpret_form_tac ctxt prec splitting taylor i THEN gen_eval_tac (approximation_conv ctxt) ctxt i - + end; diff -r f6ce08859d4c -r d4b89572ae71 src/HOL/Decision_Procs/approximation_generator.ML --- a/src/HOL/Decision_Procs/approximation_generator.ML Thu Sep 22 15:44:47 2016 +0100 +++ b/src/HOL/Decision_Procs/approximation_generator.ML Thu Sep 22 15:56:37 2016 +0100 @@ -55,6 +55,7 @@ | mapprox_floatarith (@{term Ln} $ a) xs = Math.ln (mapprox_floatarith a xs) | mapprox_floatarith (@{term Power} $ a $ n) xs = Math.pow (mapprox_floatarith a xs, Real.fromInt (nat_of_term n)) + | mapprox_floatarith (@{term Floor} $ a) xs = Real.fromInt (floor (mapprox_floatarith a xs)) | mapprox_floatarith (@{term Var} $ n) xs = nth xs (nat_of_term n) | mapprox_floatarith (@{term Num} $ m) _ = mapprox_float m | mapprox_floatarith t _ = raise TERM ("mapprox_floatarith", [t]) @@ -130,7 +131,13 @@ (map (fn t => mk_Some @{typ "float * float"} $ HOLogic.mk_prod (t, t)) ts)) $ @{term "[] :: nat list"} in - (if mapprox_form eps e (map (real_of_Float o fst) rs) + (if + mapprox_form eps e (map (real_of_Float o fst) rs) + handle + General.Overflow => false + | General.Domain => false + | General.Div => false + | IEEEReal.Unordered => false then let val ts = map (fn x => snd x ()) rs @@ -154,19 +161,12 @@ "a = b \ a \ b \ b \ a" "(p \ q) \ \p \ q" "(p \ q) \ (p \ q) \ (q \ p)" - "\ (a < b) \ b \ a" - "\ (a \ b) \ b < a" - "\ (p \ q) \ \ p \ \ q" - "\ (p \ q) \ \ p \ \ q" - "\ \ q \ q" by auto} -val form_equations = @{thms interpret_form_equations}; - fun reify_goal ctxt t = HOLogic.mk_not t |> conv_term ctxt (rewrite_with ctxt preproc_form_eqs) - |> conv_term ctxt (Reification.conv ctxt form_equations) + |> Approximation.reify_form ctxt |> dest_interpret_form ||> HOLogic.dest_list diff -r f6ce08859d4c -r d4b89572ae71 src/HOL/Decision_Procs/ex/Approximation_Ex.thy --- a/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Thu Sep 22 15:44:47 2016 +0100 +++ b/src/HOL/Decision_Procs/ex/Approximation_Ex.thy Thu Sep 22 15:56:37 2016 +0100 @@ -78,6 +78,10 @@ lemma "x \ { 0 .. 1 :: real } \ x\<^sup>2 \ x" by (approximation 30 splitting: x=1 taylor: x = 3) -approximate "10" +lemma "(n::real) \ {32 .. 62} \ \log 2 (2 * (\n\ div 2) + 1)\ = \log 2 (\n\ + 1)\" + unfolding eq_iff + by (approximation 20) + +approximate 10 end diff -r f6ce08859d4c -r d4b89572ae71 src/HOL/Library/LaTeXsugar.thy --- a/src/HOL/Library/LaTeXsugar.thy Thu Sep 22 15:44:47 2016 +0100 +++ b/src/HOL/Library/LaTeXsugar.thy Thu Sep 22 15:56:37 2016 +0100 @@ -10,15 +10,15 @@ (* LOGIC *) notation (latex output) - If ("(\<^raw:\textsf{>if\<^raw:}> (_)/ \<^raw:\textsf{>then\<^raw:}> (_)/ \<^raw:\textsf{>else\<^raw:}> (_))" 10) + If ("(\<^latex>\\\textsf{\if\<^latex>\}\ (_)/ \<^latex>\\\textsf{\then\<^latex>\}\ (_)/ \<^latex>\\\textsf{\else\<^latex>\}\ (_))" 10) syntax (latex output) "_Let" :: "[letbinds, 'a] => 'a" - ("(\<^raw:\textsf{>let\<^raw:}> (_)/ \<^raw:\textsf{>in\<^raw:}> (_))" 10) + ("(\<^latex>\\\textsf{\let\<^latex>\}\ (_)/ \<^latex>\\\textsf{\in\<^latex>\}\ (_))" 10) "_case_syntax":: "['a, cases_syn] => 'b" - ("(\<^raw:\textsf{>case\<^raw:}> _ \<^raw:\textsf{>of\<^raw:}>/ _)" 10) + ("(\<^latex>\\\textsf{\case\<^latex>\}\ _ \<^latex>\\\textsf{\of\<^latex>\}\/ _)" 10) (* SETS *) @@ -59,41 +59,41 @@ (* nth *) notation (latex output) - nth ("_\<^raw:\ensuremath{_{[\mathit{>_\<^raw:}]}}>" [1000,0] 1000) + nth ("_\<^latex>\\\ensuremath{_{[\\mathit{\_\<^latex>\}]}}\" [1000,0] 1000) (* DUMMY *) -consts DUMMY :: 'a ("\<^raw:\_>") +consts DUMMY :: 'a ("\<^latex>\\\_\") (* THEOREMS *) notation (Rule output) - Pure.imp ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>") + Pure.imp ("\<^latex>\\\mbox{}\\inferrule{\\mbox{\_\<^latex>\}}\\<^latex>\{\\mbox{\_\<^latex>\}}\") syntax (Rule output) "_bigimpl" :: "asms \ prop \ prop" - ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>") + ("\<^latex>\\\mbox{}\\inferrule{\_\<^latex>\}\\<^latex>\{\\mbox{\_\<^latex>\}}\") "_asms" :: "prop \ asms \ asms" - ("\<^raw:\mbox{>_\<^raw:}\\>/ _") + ("\<^latex>\\\mbox{\_\<^latex>\}\\\\\/ _") - "_asm" :: "prop \ asms" ("\<^raw:\mbox{>_\<^raw:}>") + "_asm" :: "prop \ asms" ("\<^latex>\\\mbox{\_\<^latex>\}\") notation (Axiom output) - "Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>") + "Trueprop" ("\<^latex>\\\mbox{}\\inferrule{\\mbox{}}{\\mbox{\_\<^latex>\}}\") notation (IfThen output) - Pure.imp ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") + Pure.imp ("\<^latex>\{\\normalsize{}\If\<^latex>\\\,}\ _/ \<^latex>\{\\normalsize \\,\then\<^latex>\\\,}\/ _.") syntax (IfThen output) "_bigimpl" :: "asms \ prop \ prop" - ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") - "_asms" :: "prop \ asms \ asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") - "_asm" :: "prop \ asms" ("\<^raw:\mbox{>_\<^raw:}>") + ("\<^latex>\{\\normalsize{}\If\<^latex>\\\,}\ _ /\<^latex>\{\\normalsize \\,\then\<^latex>\\\,}\/ _.") + "_asms" :: "prop \ asms \ asms" ("\<^latex>\\\mbox{\_\<^latex>\}\ /\<^latex>\{\\normalsize \\,\and\<^latex>\\\,}\/ _") + "_asm" :: "prop \ asms" ("\<^latex>\\\mbox{\_\<^latex>\}\") notation (IfThenNoBox output) - Pure.imp ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") + Pure.imp ("\<^latex>\{\\normalsize{}\If\<^latex>\\\,}\ _/ \<^latex>\{\\normalsize \\,\then\<^latex>\\\,}\/ _.") syntax (IfThenNoBox output) "_bigimpl" :: "asms \ prop \ prop" - ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.") - "_asms" :: "prop \ asms \ asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _") + ("\<^latex>\{\\normalsize{}\If\<^latex>\\\,}\ _ /\<^latex>\{\\normalsize \\,\then\<^latex>\\\,}\/ _.") + "_asms" :: "prop \ asms \ asms" ("_ /\<^latex>\{\\normalsize \\,\and\<^latex>\\\,}\/ _") "_asm" :: "prop \ asms" ("_") setup\ diff -r f6ce08859d4c -r d4b89572ae71 src/HOL/Library/OptionalSugar.thy --- a/src/HOL/Library/OptionalSugar.thy Thu Sep 22 15:44:47 2016 +0100 +++ b/src/HOL/Library/OptionalSugar.thy Thu Sep 22 15:56:37 2016 +0100 @@ -27,7 +27,7 @@ (* append *) syntax (latex output) - "_appendL" :: "'a list \ 'a list \ 'a list" (infixl "\<^raw:\isacharat>" 65) + "_appendL" :: "'a list \ 'a list \ 'a list" (infixl "\<^latex>\\\isacharat\" 65) translations "_appendL xs ys" <= "xs @ ys" "_appendL (_appendL xs ys) zs" <= "_appendL xs (_appendL ys zs)" @@ -36,8 +36,8 @@ (* deprecated, use thm with style instead, will be removed *) (* aligning equations *) notation (tab output) - "HOL.eq" ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and - "Pure.eq" ("(_) \<^raw:}\putisatab\isa{\ >\\<^raw:}\putisatab\isa{> (_)") + "HOL.eq" ("(_) \<^latex>\}\\putisatab\\isa{\\ \=\<^latex>\}\\putisatab\\isa{\ (_)" [50,49] 50) and + "Pure.eq" ("(_) \<^latex>\}\\putisatab\\isa{\\ \\\<^latex>\}\\putisatab\\isa{\ (_)") (* Let *) translations diff -r f6ce08859d4c -r d4b89572ae71 src/HOL/Set_Interval.thy --- a/src/HOL/Set_Interval.thy Thu Sep 22 15:44:47 2016 +0100 +++ b/src/HOL/Set_Interval.thy Thu Sep 22 15:56:37 2016 +0100 @@ -1609,13 +1609,13 @@ syntax (latex_sum output) "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" - ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10) + ("(3\<^latex>\$\\sum_{\_ = _\<^latex>\}^{\_\<^latex>\}$\ _)" [0,0,0,10] 10) "_from_upto_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" - ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10) + ("(3\<^latex>\$\\sum_{\_ = _\<^latex>\}^{<\_\<^latex>\}$\ _)" [0,0,0,10] 10) "_upt_setsum" :: "idt \ 'a \ 'b \ 'b" - ("(3\<^raw:$\sum_{>_ < _\<^raw:}$> _)" [0,0,10] 10) + ("(3\<^latex>\$\\sum_{\_ < _\<^latex>\}$\ _)" [0,0,10] 10) "_upto_setsum" :: "idt \ 'a \ 'b \ 'b" - ("(3\<^raw:$\sum_{>_ \ _\<^raw:}$> _)" [0,0,10] 10) + ("(3\<^latex>\$\\sum_{\_ \ _\<^latex>\}$\ _)" [0,0,10] 10) syntax "_from_to_setsum" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10) @@ -2013,13 +2013,13 @@ syntax (latex_prod output) "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" - ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10) + ("(3\<^latex>\$\\prod_{\_ = _\<^latex>\}^{\_\<^latex>\}$\ _)" [0,0,0,10] 10) "_from_upto_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" - ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{<>_\<^raw:}$> _)" [0,0,0,10] 10) + ("(3\<^latex>\$\\prod_{\_ = _\<^latex>\}^{<\_\<^latex>\}$\ _)" [0,0,0,10] 10) "_upt_setprod" :: "idt \ 'a \ 'b \ 'b" - ("(3\<^raw:$\prod_{>_ < _\<^raw:}$> _)" [0,0,10] 10) + ("(3\<^latex>\$\\prod_{\_ < _\<^latex>\}$\ _)" [0,0,10] 10) "_upto_setprod" :: "idt \ 'a \ 'b \ 'b" - ("(3\<^raw:$\prod_{>_ \ _\<^raw:}$> _)" [0,0,10] 10) + ("(3\<^latex>\$\\prod_{\_ \ _\<^latex>\}$\ _)" [0,0,10] 10) syntax "_from_to_setprod" :: "idt \ 'a \ 'a \ 'b \ 'b" ("(3\_ = _.._./ _)" [0,0,0,10] 10) diff -r f6ce08859d4c -r d4b89572ae71 src/HOL/Tools/Sledgehammer/sledgehammer_util.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Sep 22 15:44:47 2016 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Sep 22 15:56:37 2016 +0100 @@ -125,8 +125,8 @@ val get = maps (Proof_Context.get_fact ctxt o fst) val keywords = Thy_Header.get_keywords' ctxt in - Source.of_string name - |> Symbol.source + Symbol.explode name + |> Source.of_list |> Token.source keywords Position.start |> Token.source_proper |> Source.source Token.stopper (Parse.thms1 >> get) diff -r f6ce08859d4c -r d4b89572ae71 src/Pure/General/symbol.ML --- a/src/Pure/General/symbol.ML Thu Sep 22 15:44:47 2016 +0100 +++ b/src/Pure/General/symbol.ML Thu Sep 22 15:56:37 2016 +0100 @@ -1,5 +1,5 @@ (* Title: Pure/General/symbol.ML - Author: Markus Wenzel, TU Muenchen + Author: Makarius Generalized characters with infinitely many named symbols. *) @@ -7,6 +7,7 @@ signature SYMBOL = sig type symbol = string + val explode: string -> symbol list val spaces: int -> string val STX: symbol val DEL: symbol @@ -41,12 +42,8 @@ val to_ascii_upper: symbol -> symbol val is_ascii_identifier: string -> bool val scan_ascii_id: string list -> string * string list - val is_raw: symbol -> bool - val decode_raw: symbol -> string - val encode_raw: string -> string datatype sym = - Char of string | UTF8 of string | Sym of string | Control of string | Raw of string | - Malformed of string | EOF + Char of string | UTF8 of string | Sym of string | Control of string | Malformed of string | EOF val decode: symbol -> sym datatype kind = Letter | Digit | Quasi | Blank | Other val kind: symbol -> kind @@ -58,8 +55,6 @@ val is_quasi_letter: symbol -> bool val is_letdig: symbol -> bool val beginning: int -> symbol list -> string - val source: (string, 'a) Source.source -> (symbol, (string, 'a) Source.source) Source.source - val explode: string -> symbol list val esc: symbol -> string val escape: string -> string val scanner: string -> (string list -> 'a * string list) -> symbol list -> 'a @@ -81,11 +76,10 @@ (*Symbols, which are considered the smallest entities of any Isabelle string, may be of the following form: - (1) ASCII symbols: a + (1) ASCII: a + (2) UTF-8: รค (2) regular symbols: \ (3) control symbols: \<^ident> - (4) raw control symbols: \<^raw:...>, where "..." may be any printable - character (excluding ".", ">"), or \<^raw000> Output is subject to the print_mode variable (default: verbatim), actual interpretation in display is up to front-end tools. @@ -191,31 +185,6 @@ val scan_ascii_id = Scan.one is_ascii_letter ^^ (Scan.many is_ascii_letdig >> implode); -(* encode_raw *) - -fun raw_chr c = - is_char c andalso - (ord space <= ord c andalso ord c <= ord "~" andalso c <> "." andalso c <> ">" - orelse ord c >= 128); - -fun encode_raw "" = "" - | encode_raw str = - let - val raw0 = enclose "\092<^raw:" ">"; - val raw1 = raw0 o implode; - val raw2 = enclose "\092<^raw" ">" o string_of_int o ord; - - fun encode cs = enc (take_prefix raw_chr cs) - and enc ([], []) = [] - | enc (cs, []) = [raw1 cs] - | enc ([], d :: ds) = raw2 d :: encode ds - | enc (cs, d :: ds) = raw1 cs :: raw2 d :: encode ds; - in - if exists_string (not o raw_chr) str then implode (encode (raw_explode str)) - else raw0 str - end; - - (* diagnostics *) fun beginning n cs = @@ -230,28 +199,15 @@ end; -(* decode_raw *) - -fun is_raw s = - String.isPrefix "\092<^raw" s andalso String.isSuffix ">" s; - -fun decode_raw s = - if not (is_raw s) then error (malformed_msg s) - else if String.isPrefix "\092<^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))))); - - (* symbol variants *) datatype sym = - Char of string | UTF8 of string | Sym of string | Control of string | Raw of string | - Malformed of string | EOF; + Char of string | UTF8 of string | Sym of string | Control of string | Malformed of string | EOF; fun decode s = if s = "" then EOF else if is_char s then Char s else if is_utf8 s then UTF8 s - else if is_raw s then Raw (decode_raw s) else if is_malformed s then Malformed s else if is_control s then Control (String.substring (s, 3, size s - 4)) else Sym (String.substring (s, 2, size s - 3)); @@ -429,65 +385,6 @@ fun is_letdig s = let val k = kind s in k = Letter orelse k = Digit orelse k = Quasi end; - -(** symbol input **) - -(* source *) - -local - -fun is_plain s = is_ascii s andalso s <> "\^M" andalso s <> "\\"; - -fun is_utf8_trailer s = is_char s andalso 128 <= ord s andalso ord s < 192; - -fun implode_pseudo_utf8 (cs as ["\192", c]) = - if ord c < 160 then chr (ord c - 128) else implode cs - | implode_pseudo_utf8 cs = implode cs; - -val scan_encoded_newline = - $$ "\^M" -- $$ "\n" >> K "\n" || - $$ "\^M" >> K "\n"; - -val scan_raw = - Scan.this_string "raw:" ^^ (Scan.many raw_chr >> implode) || - Scan.this_string "raw" ^^ (Scan.many1 is_ascii_digit >> implode); - -val scan_total = - Scan.one is_plain || - Scan.one is_utf8 ::: Scan.many is_utf8_trailer >> implode_pseudo_utf8 || - scan_encoded_newline || - ($$ "\\" ^^ $$ "<" ^^ - (($$ "^" ^^ Scan.optional (scan_raw || scan_ascii_id) "" || Scan.optional scan_ascii_id "") ^^ - Scan.optional ($$ ">") "")) || - Scan.one not_eof; - -in - -fun source src = Source.source stopper (Scan.bulk scan_total) src; - -end; - - -(* explode *) - -local - -fun no_explode [] = true - | no_explode ("\\" :: "<" :: _) = false - | no_explode ("\^M" :: _) = false - | no_explode (c :: cs) = is_ascii c andalso no_explode cs; - -in - -fun sym_explode str = - let val chs = raw_explode str in - if no_explode chs then chs - else Source.exhaust (source (Source.of_list chs)) - end; - -end; - - (* escape *) val esc = fn s => @@ -495,7 +392,7 @@ else if is_utf8 s then translate_string (fn c => "\\" ^ string_of_int (ord c)) s else "\\" ^ s; -val escape = implode o map esc o sym_explode; +val escape = implode o map esc o Symbol.explode; @@ -523,12 +420,12 @@ val split_words = scanner "Bad text" (Scan.repeat scan_word >> map_filter I); -val explode_words = split_words o sym_explode; +val explode_words = split_words o Symbol.explode; (* blanks *) -val trim_blanks = sym_explode #> trim is_blank #> implode; +val trim_blanks = Symbol.explode #> trim is_blank #> implode; (* bump string -- treat as base 26 or base 1 numbers *) @@ -539,7 +436,7 @@ | symbolic_end [] = false; fun bump_init str = - if symbolic_end (rev (sym_explode str)) then str ^ "'" + if symbolic_end (rev (Symbol.explode str)) then str ^ "'" else str ^ "a"; fun bump_string str = @@ -551,7 +448,7 @@ then chr (ord s + 1) :: ss else "a" :: s :: ss; - val (ss, qs) = apfst rev (take_suffix is_quasi (sym_explode str)); + val (ss, qs) = apfst rev (take_suffix is_quasi (Symbol.explode str)); val ss' = if symbolic_end ss then "'" :: ss else bump ss; in implode (rev ss' @ qs) end; @@ -574,11 +471,11 @@ val xsymbolsN = "xsymbols"; -fun output s = (s, sym_length (sym_explode s)); +fun output s = (s, sym_length (Symbol.explode s)); (*final declarations of this structure!*) -val explode = sym_explode; +val explode = Symbol.explode; val length = sym_length; end; diff -r f6ce08859d4c -r d4b89572ae71 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Thu Sep 22 15:44:47 2016 +0100 +++ b/src/Pure/General/symbol.scala Thu Sep 22 15:56:37 2016 +0100 @@ -64,9 +64,7 @@ /* symbol matching */ private val symbol_total = new Regex("""(?xs) - [\ud800-\udbff][\udc00-\udfff] | \r\n | - \\ < (?: \^raw: [\x20-\x7e\u0100-\uffff && [^.>]]* | \^? ([A-Za-z][A-Za-z0-9_']*)? ) >? | - .""") + [\ud800-\udbff][\udc00-\udfff] | \r\n | \\ < \^? ([A-Za-z][A-Za-z0-9_']*)? >? | .""") private def is_plain(c: Char): Boolean = !(c == '\r' || c == '\\' || Character.isHighSurrogate(c)) diff -r f6ce08859d4c -r d4b89572ae71 src/Pure/General/symbol_explode.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/General/symbol_explode.ML Thu Sep 22 15:56:37 2016 +0100 @@ -0,0 +1,53 @@ +(* Title: Pure/General/symbol_explode.ML + Author: Makarius + +String explode operation for Isabelle symbols (see also symbol.ML). +*) + +structure Symbol: sig val explode: string -> string list end = +struct + +fun is_ascii_letter c = #"A" <= c andalso c <= #"Z" orelse #"a" <= c andalso c <= #"z"; +fun is_ascii_letdig c = + is_ascii_letter c orelse #"0" <= c andalso c <= #"9" orelse c = #"_" orelse c = #"'"; + +fun is_utf8 c = c >= #"\128"; +fun is_utf8_trailer c = #"\128" <= c andalso c < #"\192"; +fun is_utf8_control c = #"\128" <= c andalso c < #"\160"; + +fun explode string = + let + fun char i = String.sub (string, i); + fun string_range i j = String.substring (string, i, j - i); + + val n = size string; + fun test pred i = i < n andalso pred (char i); + fun many pred i = if test pred i then many pred (i + 1) else i; + fun maybe pred i = if test pred i then i + 1 else i; + fun maybe_char c = maybe (fn c' => c = c'); + fun maybe_ascii_id i = if test is_ascii_letter i then many is_ascii_letdig (i + 1) else i; + + fun scan i = + if i < n then + let val ch = char i in + (*encoded newline*) + if ch = #"\^M" then "\n" :: scan (maybe_char #"\n" (i + 1)) + (*pseudo utf8: encoded ascii control*) + else if ch = #"\192" andalso + test is_utf8_control (i + 1) andalso not (test is_utf8 (i + 2)) + then chr (Char.ord (char (i + 1)) - 128) :: scan (i + 2) + (*utf8*) + else if is_utf8 ch then + let val j = many is_utf8_trailer (i + 1) + in string_range i j :: scan j end + (*named symbol*) + else if ch = #"\\" andalso test (fn c => c = #"<") (i + 1) then + let val j = (i + 2) |> maybe_char #"^" |> maybe_ascii_id |> maybe_char #">" + in string_range i j :: scan j end + (*single character*) + else String.str ch :: scan (i + 1) + end + else []; + in scan 0 end; + +end; diff -r f6ce08859d4c -r d4b89572ae71 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Thu Sep 22 15:44:47 2016 +0100 +++ b/src/Pure/Isar/outer_syntax.ML Thu Sep 22 15:56:37 2016 +0100 @@ -220,17 +220,17 @@ in -fun parse thy pos str = - Source.of_string str - |> Symbol.source - |> Token.source (Thy_Header.get_keywords thy) pos - |> commands_source thy - |> Source.exhaust; +fun parse thy pos = + Symbol.explode + #> Source.of_list + #> Token.source (Thy_Header.get_keywords thy) pos + #> commands_source thy + #> Source.exhaust; -fun parse_tokens thy toks = - Source.of_list toks - |> commands_source thy - |> Source.exhaust; +fun parse_tokens thy = + Source.of_list + #> commands_source thy + #> Source.exhaust; end; diff -r f6ce08859d4c -r d4b89572ae71 src/Pure/Isar/token.ML --- a/src/Pure/Isar/token.ML Thu Sep 22 15:44:47 2016 +0100 +++ b/src/Pure/Isar/token.ML Thu Sep 22 15:56:37 2016 +0100 @@ -650,8 +650,8 @@ (* explode *) fun explode keywords pos = - Source.of_string #> - Symbol.source #> + Symbol.explode #> + Source.of_list #> source keywords pos #> Source.exhaust; diff -r f6ce08859d4c -r d4b89572ae71 src/Pure/ML/ml_lex.ML --- a/src/Pure/ML/ml_lex.ML Thu Sep 22 15:44:47 2016 +0100 +++ b/src/Pure/ML/ml_lex.ML Thu Sep 22 15:56:37 2016 +0100 @@ -351,7 +351,7 @@ Symbol_Pos.source (Position.line 1) src |> Source.source Symbol_Pos.stopper (Scan.recover (Scan.bulk (!!! "bad input" scan_ml)) recover); -val tokenize = Source.of_string #> Symbol.source #> source #> Source.exhaust; +val tokenize = Symbol.explode #> Source.of_list #> source #> Source.exhaust; val read_pos = gen_read false; diff -r f6ce08859d4c -r d4b89572ae71 src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Thu Sep 22 15:44:47 2016 +0100 +++ b/src/Pure/ROOT.ML Thu Sep 22 15:56:37 2016 +0100 @@ -10,6 +10,7 @@ ML_file "System/distribution.ML"; ML_file "General/basics.ML"; +ML_file "General/symbol_explode.ML"; ML_file "Concurrent/multithreading.ML"; ML_file "Concurrent/unsynchronized.ML"; diff -r f6ce08859d4c -r d4b89572ae71 src/Pure/Syntax/syntax_ext.ML --- a/src/Pure/Syntax/syntax_ext.ML Thu Sep 22 15:44:47 2016 +0100 +++ b/src/Pure/Syntax/syntax_ext.ML Thu Sep 22 15:56:37 2016 +0100 @@ -251,9 +251,10 @@ val is_meta = member (op =) ["(", ")", "/", "_", "\", Symbol.open_, Symbol.close]; -val scan_delim_char = - $$ "'" |-- scan_one ((not o Symbol.is_blank) andf Symbol.not_eof) || - scan_one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof); +val scan_delim = + scan_one Symbol.is_control ::: Symbol_Pos.scan_cartouche "Mixfix error: " || + $$ "'" |-- scan_one ((not o Symbol.is_blank) andf Symbol.not_eof) >> single || + scan_one ((not o is_meta) andf (not o Symbol.is_blank) andf Symbol.not_eof) >> single; val scan_sym = $$ "_" >> K (Argument ("", 0)) || @@ -265,7 +266,7 @@ $$ "/" -- $$ "/" >> K (Brk ~1) || $$ "/" |-- scan_many Symbol.is_space >> (Brk o length) || scan_many1 Symbol.is_space >> (Space o Symbol_Pos.content) || - Scan.repeat1 scan_delim_char >> (Delim o Symbol_Pos.content); + Scan.repeat1 scan_delim >> (Delim o Symbol_Pos.content o flat); val scan_symb = Scan.trace scan_sym >> (fn (syms, trace) => SOME (syms, #1 (Symbol_Pos.range trace))) || diff -r f6ce08859d4c -r d4b89572ae71 src/Pure/Thy/html.ML --- a/src/Pure/Thy/html.ML Thu Sep 22 15:44:47 2016 +0100 +++ b/src/Pure/Thy/html.ML Thu Sep 22 15:56:37 2016 +0100 @@ -48,11 +48,9 @@ val no_symbols = make_symbols []; fun output_sym (Symbols tab) s = - if Symbol.is_raw s then Symbol.decode_raw s - else - (case Symtab.lookup tab s of - SOME x => x - | NONE => XML.text s); + (case Symtab.lookup tab s of + SOME x => x + | NONE => XML.text s); end; diff -r f6ce08859d4c -r d4b89572ae71 src/Pure/Thy/latex.ML --- a/src/Pure/Thy/latex.ML Thu Sep 22 15:44:47 2016 +0100 +++ b/src/Pure/Thy/latex.ML Thu Sep 22 15:56:37 2016 +0100 @@ -7,6 +7,9 @@ signature LATEX = sig val output_ascii: string -> string + val latex_control: Symbol.symbol + val is_latex_control: Symbol.symbol -> bool + val embed_raw: string -> string val output_known_symbols: (string -> bool) * (string -> bool) -> Symbol.symbol list -> string val output_symbols: Symbol.symbol list -> string @@ -41,6 +44,11 @@ (* output symbols *) +val latex_control = "\<^latex>"; +fun is_latex_control s = s = latex_control; + +val embed_raw = prefix latex_control o cartouche; + local val char_table = @@ -95,13 +103,26 @@ | Symbol.UTF8 s => s | Symbol.Sym s => if known_sym s then enclose "{\\isasym" "}" s else output_chrs sym | Symbol.Control s => if known_ctrl s then enclose "\\isactrl" " " s else output_chrs sym - | Symbol.Raw s => s | Symbol.Malformed s => error (Symbol.malformed_msg s) | Symbol.EOF => error "Bad EOF symbol"); +fun scan_latex known = + Scan.one (is_latex_control o Symbol_Pos.symbol) |-- + Symbol_Pos.scan_cartouche_content "Embedded LaTeX: " >> (implode o map Symbol_Pos.symbol) || + Scan.one (Symbol.not_eof o Symbol_Pos.symbol) >> (output_known_sym known o Symbol_Pos.symbol); + +fun read_latex known syms = + (case Scan.read Symbol_Pos.stopper (Scan.repeat (scan_latex known)) + (map (rpair Position.none) syms) of + SOME ss => implode ss + | NONE => error ("Malformed embedded LaTeX: " ^ quote (Symbol.beginning 10 syms))); + in -val output_known_symbols = implode oo (map o output_known_sym); +fun output_known_symbols known syms = + if exists is_latex_control syms then read_latex known syms + else implode (map (output_known_sym known) syms); + val output_symbols = output_known_symbols (K true, K true); val output_syms = output_symbols o Symbol.explode; @@ -192,7 +213,7 @@ fun latex_indent "" _ = "" | latex_indent s _ = enclose "\\isaindent{" "}" s; -val _ = Output.add_mode latexN latex_output Symbol.encode_raw; +val _ = Output.add_mode latexN latex_output embed_raw; val _ = Markup.add_mode latexN latex_markup; val _ = Pretty.add_mode latexN latex_indent; diff -r f6ce08859d4c -r d4b89572ae71 src/Pure/Thy/thy_header.ML --- a/src/Pure/Thy/thy_header.ML Thu Sep 22 15:44:47 2016 +0100 +++ b/src/Pure/Thy/thy_header.ML Thu Sep 22 15:56:37 2016 +0100 @@ -168,11 +168,10 @@ val header = (Scan.repeat heading -- Parse.command theoryN -- Parse.tags) |-- Parse.!!! args; -fun token_source pos str = - str - |> Source.of_string_limited 8000 - |> Symbol.source - |> Token.source_strict bootstrap_keywords pos; +fun token_source pos = + Symbol.explode + #> Source.of_list + #> Token.source_strict bootstrap_keywords pos; fun read_source pos source = let val res =