# HG changeset patch
# User schirmer
# Date 1075109642 -3600
# Node ID ad2f5da643b47bb788f608e68955b341cd971a95
# Parent  e654599b114ec2dab0b37000265cda39240a5948
* 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

diff -r e654599b114e -r ad2f5da643b4 NEWS
--- a/NEWS	Sun Jan 25 00:42:22 2004 +0100
+++ b/NEWS	Mon Jan 26 10:34:02 2004 +0100
@@ -29,6 +29,13 @@
   PG and LaTeX, text between \<^bsup> and \<^esup> in superscript. The
   new control characters are not identifier parts.
 
+* Pure: Control-symbols of the form \<^raw...> will literally print the
+  content of ... to the latex file instead of \isacntrl... . The ... 
+  accepts all printable characters excluding the end bracket >.
+
+* Pure: Symbols may only start with one backslash: \<...>. \\<...> is no 
+  longer accepted by the scanner.
+
 * Pure: Using new Isar command "finalconsts" (or the ML functions
   Theory.add_finals or Theory.add_finals_i) it is now possible to
   declare constants "final", which prevents their being given a definition
diff -r e654599b114e -r ad2f5da643b4 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sun Jan 25 00:42:22 2004 +0100
+++ b/src/HOL/HOL.thy	Mon Jan 26 10:34:02 2004 +0100
@@ -96,7 +96,7 @@
   "EX "         :: "[idts, bool] => bool"                ("(3\<exists>_./ _)" [0, 10] 10)
   "EX! "        :: "[idts, bool] => bool"                ("(3\<exists>!_./ _)" [0, 10] 10)
   "_case1"      :: "['a, 'b] => case_syn"                ("(2_ \<Rightarrow>/ _)" 10)
-(*"_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \\<orelse> _")*)
+(*"_case2"      :: "[case_syn, cases_syn] => cases_syn"  ("_/ \<orelse> _")*)
 
 syntax (xsymbols output)
   "_not_equal"  :: "['a, 'a] => bool"                    (infix "\<noteq>" 50)
diff -r e654599b114e -r ad2f5da643b4 src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Sun Jan 25 00:42:22 2004 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy	Mon Jan 26 10:34:02 2004 +0100
@@ -11,7 +11,7 @@
 
 constdefs
 
-  FreeUltrafilterNat   :: "nat set set"    ("\\<U>")
+  FreeUltrafilterNat   :: "nat set set"    ("\<U>")
     "FreeUltrafilterNat == (SOME U. U \<in> FreeUltrafilter (UNIV:: nat set))"
 
   hyprel :: "((nat=>real)*(nat=>real)) set"
diff -r e654599b114e -r ad2f5da643b4 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Sun Jan 25 00:42:22 2004 +0100
+++ b/src/HOL/Transitive_Closure.thy	Mon Jan 26 10:34:02 2004 +0100
@@ -39,9 +39,9 @@
   "r^=" == "r \<union> Id"
 
 syntax (xsymbols)
-  rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\\<^sup>*)" [1000] 999)
-  trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\\<^sup>+)" [1000] 999)
-  "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\\<^sup>=)" [1000] 999)
+  rtrancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>*)" [1000] 999)
+  trancl :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>+)" [1000] 999)
+  "_reflcl" :: "('a \<times> 'a) set => ('a \<times> 'a) set"    ("(_\<^sup>=)" [1000] 999)
 
 
 subsection {* Reflexive-transitive closure *}
diff -r e654599b114e -r ad2f5da643b4 src/HOL/UNITY/Comp/AllocBase.thy
--- a/src/HOL/UNITY/Comp/AllocBase.thy	Sun Jan 25 00:42:22 2004 +0100
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Mon Jan 26 10:34:02 2004 +0100
@@ -71,13 +71,13 @@
 declare setsum_cong [cong]
 
 lemma bag_of_sublist_lemma:
-     "(\\<Sum>i: A Int lessThan k. {#if i<k then f i else g i#}) =  
-      (\\<Sum>i: A Int lessThan k. {#f i#})"
+     "(\<Sum>i: A Int lessThan k. {#if i<k then f i else g i#}) =  
+      (\<Sum>i: A Int lessThan k. {#f i#})"
 by (rule setsum_cong, auto)
 
 lemma bag_of_sublist:
      "bag_of (sublist l A) =  
-      (\\<Sum>i: A Int lessThan (length l). {# l!i #})"
+      (\<Sum>i: A Int lessThan (length l). {# l!i #})"
 apply (rule_tac xs = l in rev_induct, simp)
 apply (simp add: sublist_append Int_insert_right lessThan_Suc nth_append 
                  bag_of_sublist_lemma plus_ac0)
@@ -101,7 +101,7 @@
 lemma bag_of_sublist_UN_disjoint [rule_format]:
      "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |]  
       ==> bag_of (sublist l (UNION I A)) =   
-          (\\<Sum>i:I. bag_of (sublist l (A i)))"
+          (\<Sum>i:I. bag_of (sublist l (A i)))"
 apply (simp del: UN_simps 
             add: UN_simps [symmetric] add: bag_of_sublist)
 apply (subst setsum_UN_disjoint, auto)
diff -r e654599b114e -r ad2f5da643b4 src/Pure/General/symbol.ML
--- a/src/Pure/General/symbol.ML	Sun Jan 25 00:42:22 2004 +0100
+++ b/src/Pure/General/symbol.ML	Mon Jan 26 10:34:02 2004 +0100
@@ -59,7 +59,7 @@
   string, may be of the following form:
     (a) ASCII symbols: a
     (b) printable symbols: \<ident>
-    (c) control symbols: \<^ident>
+    (c) control symbols: \<^ctrlident>
 
   output is subject to the print_mode variable (default: verbatim),
   actual interpretation in display is up to front-end tools;
@@ -156,6 +156,9 @@
   is_ext_letter s orelse
   is_symbolic s;
 
+fun is_ctrl_letter s =
+  size s = 1 andalso ord space <= ord s andalso ord s <= ord "~" andalso s <> ">";
+
 fun is_identifier s =
   case (explode s) of
       [] => false
@@ -203,14 +206,14 @@
 (* scan *)
 
 val scan_id = Scan.one is_letter ^^ (Scan.any is_letdig >> implode);
+val scan_ctrlid = Scan.one is_letter ^^ (Scan.any is_ctrl_letter >> implode);
 
 val scan =
-  ($$ "\\" --| Scan.optional ($$ "\\") "") ^^ $$ "<" ^^
+  $$ "\\" ^^ $$ "<" ^^
     !! (fn (cs, _) => "Malformed symbolic character specification: \\" ^ "<" ^ beginning cs)
-      (Scan.optional ($$ "^") "" ^^ scan_id ^^ $$ ">") ||
+       ((($$ "^" ^^ scan_ctrlid) || scan_id) ^^ $$ ">") ||
   Scan.one not_eof;
 
-
 (* source *)
 
 val recover = Scan.any ((not o is_blank) andf not_eof) >> K [malformed];
diff -r e654599b114e -r ad2f5da643b4 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Sun Jan 25 00:42:22 2004 +0100
+++ b/src/Pure/Thy/latex.ML	Mon Jan 26 10:34:02 2004 +0100
@@ -69,7 +69,8 @@
   if size s = 1 then output_chr s
   else
     (case explode s of
-      "\\" :: "<" :: "^" :: cs => "\\isactrl" ^ implode (#1 (Library.split_last cs)) ^ " "
+      "\\" :: "<" :: "^" :: "r"::"a"::"w":: cs => implode (#1 (Library.split_last cs)) ^ " "
+    | "\\" :: "<" :: "^" :: cs => "\\isactrl" ^ implode (#1 (Library.split_last cs)) ^ " "
     | "\\" :: "<" :: cs => "{\\isasym" ^ implode (#1 (Library.split_last cs)) ^ "}"
     | _ => sys_error "output_sym");