# HG changeset patch
# User krauss
# Date 1296590992 -3600
# Node ID e29ea98a76ce603f8c7d9aa7cb4aec99c19908cb
# Parent  fa0da47131d213b4049d94387bdd3b0e61f639a1
term style 'isub': ad-hoc subscripting of variables that end with digits (x1, x23, ...)

diff -r fa0da47131d2 -r e29ea98a76ce NEWS
--- a/NEWS	Mon Jan 31 23:53:07 2011 +0100
+++ b/NEWS	Tue Feb 01 21:09:52 2011 +0100
@@ -4,6 +4,10 @@
 New in this Isabelle version
 ----------------------------
 
+*** Document preparation ***
+
+* New term style "isub" as ad-hoc conversion of variables x1, y23 into
+subscripted form x\<^isub>1, y\<^isub>2\<^isub>3.
 
 
 New in Isabelle2011 (January 2011)
diff -r fa0da47131d2 -r e29ea98a76ce src/Pure/Thy/term_style.ML
--- a/src/Pure/Thy/term_style.ML	Mon Jan 31 23:53:07 2011 +0100
+++ b/src/Pure/Thy/term_style.ML	Tue Feb 01 21:09:52 2011 +0100
@@ -94,11 +94,30 @@
       " in propositon: " ^ Syntax.string_of_term ctxt t)
   end);
 
+fun isub_symbols (d :: s :: ss) =
+      if Symbol.is_ascii_digit d andalso not (String.isPrefix ("\\<^") s)
+      then d :: "\\<^isub>" :: isub_symbols (s :: ss)
+      else d :: s :: ss
+  | isub_symbols cs = cs;
+
+val isub_name = implode o rev o isub_symbols o rev o Symbol.explode;
+
+fun isub_term (Free (n, T)) = Free (isub_name n, T)
+  | isub_term (Var ((n, idx), T)) =
+      if idx <> 0 then Var ((isub_name (n ^ string_of_int idx), 0), T)
+      else Var ((isub_name n, 0), T)
+  | isub_term (t $ u) = isub_term t $ isub_term u
+  | isub_term (Abs (n, T, b)) = Abs (isub_name n, T, isub_term b)
+  | isub_term t = t;
+
+val style_isub = Scan.succeed (K isub_term);
+
 val _ = Context.>> (Context.map_theory
  (setup "lhs" (style_lhs_rhs fst) #>
   setup "rhs" (style_lhs_rhs snd) #>
   setup "prem" style_prem #>
   setup "concl" (Scan.succeed (K Logic.strip_imp_concl)) #>
+  setup "isub" style_isub #>
   setup "prem1" (style_parm_premise 1) #>
   setup "prem2" (style_parm_premise 2) #>
   setup "prem3" (style_parm_premise 3) #>