index syntax: support for general expressions (input only);

--- a/src/Pure/Isar/proof_context.ML	Fri Apr 23 20:50:51 2004 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Apr 23 20:52:04 2004 +0200
@@ -309,6 +309,21 @@
   else raise ERROR_MESSAGE ("Illegal reference to implicit structure #" ^ string_of_int i);
 
 
+(* parse translations *)
+
+fun fixed_tr x = (fixedN ^ x, curry Term.list_comb (Syntax.free x));
+
+fun index_tr struct_ (Const ("_noindex", _)) = Syntax.free (struct_ 1)
+  | index_tr struct_ (t as (Const ("_index", _) $ Const (s, _))) =
+      Syntax.free (struct_
+        (case Syntax.read_nat s of Some n => n | None => raise TERM ("index_tr", [t])))
+  | index_tr _ (Const ("_indexlogic", _) $ t) = t
+  | index_tr _ t = raise TERM ("index_tr", [t]);
+
+fun struct_tr structs [idx] = index_tr (the_struct structs) idx
+  | struct_tr _ ts = raise TERM ("struct_tr", ts);
+
+
 (* print (ast) translations *)
 
 fun index_tr' 1 = Syntax.const "_noindex"
@@ -341,19 +356,6 @@
   | struct_ast_tr' _ _ = raise Match;
 
 
-(* parse translations *)
-
-fun fixed_tr x = (fixedN ^ x, curry Term.list_comb (Syntax.free x));
-
-fun index_tr (Const ("_noindex", _)) = 1
-  | index_tr (t as (Const ("_index", _) $ Const (s, _))) =
-      (case Syntax.read_nat s of Some n => n | None => raise TERM ("index_tr", [t]))
-  | index_tr t = raise TERM ("index_tr", [t]);
-
-fun struct_tr structs (idx :: ts) = Syntax.free (the_struct structs (index_tr idx))
-  | struct_tr _ ts = raise TERM ("struct_tr", ts);
-
-
 (* add syntax *)
 
 fun mixfix_type mx = replicate (Syntax.mixfix_args mx) TypeInfer.logicT ---> TypeInfer.logicT;

--- a/src/Pure/Syntax/mixfix.ML	Fri Apr 23 20:50:51 2004 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Fri Apr 23 20:52:04 2004 +0200
@@ -210,39 +210,40 @@
     "asms", SynExt.any, SynExt.sprop, "num_const", "index", "struct"]);
 
 val pure_syntax =
- [("_lambda",      "[pttrns, 'a] => logic",         Mixfix ("(3%_./ _)", [0, 3], 3)),
-  ("_abs",         "'a",                            NoSyn),
-  ("",             "'a => " ^ SynExt.args,          Delimfix "_"),
-  ("_args",        "['a, " ^ SynExt.args ^ "] => " ^ SynExt.args, Delimfix "_,/ _"),
-  ("",             "id => idt",                     Delimfix "_"),
-  ("_idtyp",       "[id, type] => idt",             Mixfix ("_::_", [], 0)),
-  ("",             "idt => idt",                    Delimfix "'(_')"),
-  ("",             "idt => idts",                   Delimfix "_"),
-  ("_idts",        "[idt, idts] => idts",           Mixfix ("_/ _", [1, 0], 0)),
-  ("",             "idt => pttrn",                  Delimfix "_"),
-  ("",             "pttrn => pttrns",               Delimfix "_"),
-  ("_pttrns",      "[pttrn, pttrns] => pttrns",     Mixfix ("_/ _", [1, 0], 0)),
-  ("",             "id => aprop",                   Delimfix "_"),
-  ("",             "longid => aprop",               Delimfix "_"),
-  ("",             "var => aprop",                  Delimfix "_"),
-  ("_DDDOT",       "aprop",                         Delimfix "..."),
-  ("_aprop",       "aprop => prop",                 Delimfix "PROP _"),
-  ("",             "prop => asms",                  Delimfix "_"),
-  ("_asms",        "[prop, asms] => asms",          Delimfix "_;/ _"),
-  ("_bigimpl",     "[asms, prop] => prop",          Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
-  ("_ofclass",     "[type, logic] => prop",         Delimfix "(1OFCLASS/(1'(_,/ _')))"),
-  ("_mk_ofclass",  "_",                             NoSyn),
-  ("_TYPE",        "type => logic",                 Delimfix "(1TYPE/(1'(_')))"),
-  ("_K",           "_",                             NoSyn),
-  ("",             "id => logic",                   Delimfix "_"),
-  ("",             "longid => logic",               Delimfix "_"),
-  ("",             "var => logic",                  Delimfix "_"),
-  ("_DDDOT",       "logic",                         Delimfix "..."),
-  ("_constify",    "num => num_const",              Delimfix "_"),
-  ("_index",       "num_const => index",            Delimfix "\\<^sub>_"),
-  ("_indexvar",    "index",                         Delimfix "'\\<index>"),
-  ("_noindex",     "index",                         Delimfix ""),
-  ("_struct",      "index => logic",                Delimfix "\\<struct>_")];
+ [("_lambda",     "[pttrns, 'a] => logic",     Mixfix ("(3%_./ _)", [0, 3], 3)),
+  ("_abs",        "'a",                        NoSyn),
+  ("",            "'a => " ^ SynExt.args,      Delimfix "_"),
+  ("_args",       "['a, " ^ SynExt.args ^ "] => " ^ SynExt.args, Delimfix "_,/ _"),
+  ("",            "id => idt",                 Delimfix "_"),
+  ("_idtyp",      "[id, type] => idt",         Mixfix ("_::_", [], 0)),
+  ("",            "idt => idt",                Delimfix "'(_')"),
+  ("",            "idt => idts",               Delimfix "_"),
+  ("_idts",       "[idt, idts] => idts",       Mixfix ("_/ _", [1, 0], 0)),
+  ("",            "idt => pttrn",              Delimfix "_"),
+  ("",            "pttrn => pttrns",           Delimfix "_"),
+  ("_pttrns",     "[pttrn, pttrns] => pttrns", Mixfix ("_/ _", [1, 0], 0)),
+  ("",            "id => aprop",               Delimfix "_"),
+  ("",            "longid => aprop",           Delimfix "_"),
+  ("",            "var => aprop",              Delimfix "_"),
+  ("_DDDOT",      "aprop",                     Delimfix "..."),
+  ("_aprop",      "aprop => prop",             Delimfix "PROP _"),
+  ("",            "prop => asms",              Delimfix "_"),
+  ("_asms",       "[prop, asms] => asms",      Delimfix "_;/ _"),
+  ("_bigimpl",    "[asms, prop] => prop",      Mixfix ("((3[| _ |])/ ==> _)", [0, 1], 1)),
+  ("_ofclass",    "[type, logic] => prop",     Delimfix "(1OFCLASS/(1'(_,/ _')))"),
+  ("_mk_ofclass", "_",                         NoSyn),
+  ("_TYPE",       "type => logic",             Delimfix "(1TYPE/(1'(_')))"),
+  ("_K",          "_",                         NoSyn),
+  ("",            "id => logic",               Delimfix "_"),
+  ("",            "longid => logic",           Delimfix "_"),
+  ("",            "var => logic",              Delimfix "_"),
+  ("_DDDOT",      "logic",                     Delimfix "..."),
+  ("_constify",   "num => num_const",          Delimfix "_"),
+  ("_index",      "num_const => index",        Delimfix "\\<^sub>_"),
+  ("_indexlogic", "logic => index",            Delimfix "\\<^bsub>_\\<^esub>"),
+  ("_indexvar",   "index",                     Delimfix "'\\<index>"),
+  ("_noindex",    "index",                     Delimfix ""),
+  ("_struct",     "index => logic",            Mixfix ("\\<struct>_", [1000], 1000))];
 
 val pure_syntax_output =
  [("Goal", "prop => prop", Mixfix ("_", [0], 0)),