* Support for raw latex output in control symbols: \<^raw...>
authorschirmer
Mon Jan 26 10:34:02 2004 +0100 (2004-01-26)
changeset 14361ad2f5da643b4
parent 14360 e654599b114e
child 14362 b378b6faf4a7
* Support for raw latex output in control symbols: \<^raw...>
* Symbols may only start with one backslash: \<...>. \\<...> is no longer
accepted by the scanner.
- Adapted some Isar-theories to fit to this policy
NEWS
src/HOL/HOL.thy
src/HOL/Hyperreal/HyperDef.thy
src/HOL/Transitive_Closure.thy
src/HOL/UNITY/Comp/AllocBase.thy
src/Pure/General/symbol.ML
src/Pure/Thy/latex.ML
     1.1 --- a/NEWS	Sun Jan 25 00:42:22 2004 +0100
     1.2 +++ b/NEWS	Mon Jan 26 10:34:02 2004 +0100
     1.3 @@ -29,6 +29,13 @@
     1.4    PG and LaTeX, text between \<^bsup> and \<^esup> in superscript. The
     1.5    new control characters are not identifier parts.
     1.6  
     1.7 +* Pure: Control-symbols of the form \<^raw...> will literally print the
     1.8 +  content of ... to the latex file instead of \isacntrl... . The ... 
     1.9 +  accepts all printable characters excluding the end bracket >.
    1.10 +
    1.11 +* Pure: Symbols may only start with one backslash: \<...>. \\<...> is no 
    1.12 +  longer accepted by the scanner.
    1.13 +
    1.14  * Pure: Using new Isar command "finalconsts" (or the ML functions
    1.15    Theory.add_finals or Theory.add_finals_i) it is now possible to
    1.16    declare constants "final", which prevents their being given a definition
     2.1 --- a/src/HOL/HOL.thy	Sun Jan 25 00:42:22 2004 +0100
     2.2 +++ b/src/HOL/HOL.thy	Mon Jan 26 10:34:02 2004 +0100
     2.3 @@ -96,7 +96,7 @@
     2.4    "EX "         :: "[idts, bool] => bool"                ("(3\<exists>_./ _)" [0, 10] 10)
     2.5    "EX! "        :: "[idts, bool] => bool"                ("(3\<exists>!_./ _)" [0, 10] 10)
     2.6    "_case1"      :: "['a, 'b] => case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
     2.7 -(*"_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \\<orelse> _")*)
     2.8 +(*"_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \<orelse> _")*)
     2.9  
    2.10  syntax (xsymbols output)
    2.11    "_not_equal"  :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
     3.1 --- a/src/HOL/Hyperreal/HyperDef.thy	Sun Jan 25 00:42:22 2004 +0100
     3.2 +++ b/src/HOL/Hyperreal/HyperDef.thy	Mon Jan 26 10:34:02 2004 +0100
     3.3 @@ -11,7 +11,7 @@
     3.4  
     3.5  constdefs
     3.6  
     3.7 -  FreeUltrafilterNat   :: "nat set set"    ("\\<U>")
     3.8 +  FreeUltrafilterNat   :: "nat set set"    ("\<U>")
     3.9      "FreeUltrafilterNat == (SOME U. U \<in> FreeUltrafilter (UNIV:: nat set))"
    3.10  
    3.11    hyprel :: "((nat=>real)*(nat=>real)) set"
     4.1 --- a/src/HOL/Transitive_Closure.thy	Sun Jan 25 00:42:22 2004 +0100
     4.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Jan 26 10:34:02 2004 +0100
     4.3 @@ -39,9 +39,9 @@
     4.4    "r^=" == "r \<union> Id"
     4.5  
     4.6  syntax (xsymbols)
     4.7 -  rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\\<^sup>*)" [1000] 999)
     4.8 -  trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\\<^sup>+)" [1000] 999)
     4.9 -  "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\\<^sup>=)" [1000] 999)
    4.10 +  rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>*)" [1000] 999)
    4.11 +  trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>+)" [1000] 999)
    4.12 +  "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>=)" [1000] 999)
    4.13  
    4.14  
    4.15  subsection {* Reflexive-transitive closure *}
     5.1 --- a/src/HOL/UNITY/Comp/AllocBase.thy	Sun Jan 25 00:42:22 2004 +0100
     5.2 +++ b/src/HOL/UNITY/Comp/AllocBase.thy	Mon Jan 26 10:34:02 2004 +0100
     5.3 @@ -71,13 +71,13 @@
     5.4  declare setsum_cong [cong]
     5.5  
     5.6  lemma bag_of_sublist_lemma:
     5.7 -     "(\\<Sum>i: A Int lessThan k. {#if i<k then f i else g i#}) =  
     5.8 -      (\\<Sum>i: A Int lessThan k. {#f i#})"
     5.9 +     "(\<Sum>i: A Int lessThan k. {#if i<k then f i else g i#}) =  
    5.10 +      (\<Sum>i: A Int lessThan k. {#f i#})"
    5.11  by (rule setsum_cong, auto)
    5.12  
    5.13  lemma bag_of_sublist:
    5.14       "bag_of (sublist l A) =  
    5.15 -      (\\<Sum>i: A Int lessThan (length l). {# l!i #})"
    5.16 +      (\<Sum>i: A Int lessThan (length l). {# l!i #})"
    5.17  apply (rule_tac xs = l in rev_induct, simp)
    5.18  apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append 
    5.19                   bag_of_sublist_lemma plus_ac0)
    5.20 @@ -101,7 +101,7 @@
    5.21  lemma bag_of_sublist_UN_disjoint [rule_format]:
    5.22       "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |]  
    5.23        ==> bag_of (sublist l (UNION I A)) =   
    5.24 -          (\\<Sum>i:I. bag_of (sublist l (A i)))"
    5.25 +          (\<Sum>i:I. bag_of (sublist l (A i)))"
    5.26  apply (simp del: UN_simps 
    5.27              add: UN_simps [symmetric] add: bag_of_sublist)
    5.28  apply (subst setsum_UN_disjoint, auto)
     6.1 --- a/src/Pure/General/symbol.ML	Sun Jan 25 00:42:22 2004 +0100
     6.2 +++ b/src/Pure/General/symbol.ML	Mon Jan 26 10:34:02 2004 +0100
     6.3 @@ -59,7 +59,7 @@
     6.4    string, may be of the following form:
     6.5      (a) ASCII symbols: a
     6.6      (b) printable symbols: \<ident>
     6.7 -    (c) control symbols: \<^ident>
     6.8 +    (c) control symbols: \<^ctrlident>
     6.9  
    6.10    output is subject to the print_mode variable (default: verbatim),
    6.11    actual interpretation in display is up to front-end tools;
    6.12 @@ -156,6 +156,9 @@
    6.13    is_ext_letter s orelse
    6.14    is_symbolic s;
    6.15  
    6.16 +fun is_ctrl_letter s =
    6.17 +  size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" andalso s <> ">";
    6.18 +
    6.19  fun is_identifier s =
    6.20    case (explode s) of
    6.21        [] => false
    6.22 @@ -203,14 +206,14 @@
    6.23  (* scan *)
    6.24  
    6.25  val scan_id = Scan.one is_letter ^^ (Scan.any is_letdig >> implode);
    6.26 +val scan_ctrlid = Scan.one is_letter ^^ (Scan.any is_ctrl_letter >> implode);
    6.27  
    6.28  val scan =
    6.29 -  ($$ "\\" --| Scan.optional ($$ "\\") "") ^^ $$ "<" ^^
    6.30 +  $$ "\\" ^^ $$ "<" ^^
    6.31      !! (fn (cs, _) => "Malformed symbolic character specification: \\" ^ "<" ^ beginning cs)
    6.32 -      (Scan.optional ($$ "^") "" ^^ scan_id ^^ $$ ">") ||
    6.33 +       ((($$ "^" ^^ scan_ctrlid) || scan_id) ^^ $$ ">") ||
    6.34    Scan.one not_eof;
    6.35  
    6.36 -
    6.37  (* source *)
    6.38  
    6.39  val recover = Scan.any ((not o is_blank) andf not_eof) >> K [malformed];
     7.1 --- a/src/Pure/Thy/latex.ML	Sun Jan 25 00:42:22 2004 +0100
     7.2 +++ b/src/Pure/Thy/latex.ML	Mon Jan 26 10:34:02 2004 +0100
     7.3 @@ -69,7 +69,8 @@
     7.4    if size s = 1 then output_chr s
     7.5    else
     7.6      (case explode s of
     7.7 -      "\\" :: "<" :: "^" :: cs => "\\isactrl" ^ implode (#1 (Library.split_last cs)) ^ " "
     7.8 +      "\\" :: "<" :: "^" :: "r"::"a"::"w":: cs => implode (#1 (Library.split_last cs)) ^ " "
     7.9 +    | "\\" :: "<" :: "^" :: cs => "\\isactrl" ^ implode (#1 (Library.split_last cs)) ^ " "
    7.10      | "\\" :: "<" :: cs => "{\\isasym" ^ implode (#1 (Library.split_last cs)) ^ "}"
    7.11      | _ => sys_error "output_sym");
    7.12