proof_general_trans (experimental);
authorwenzelm
Sun Nov 29 13:16:47 1998 +0100 (1998-11-29)
changeset 59899670dae0143d
parent 5988 1a2285f3db47
child 5990 8b6de9bd7d72
proof_general_trans (experimental);
src/Pure/Syntax/token_trans.ML
     1.1 --- a/src/Pure/Syntax/token_trans.ML	Sun Nov 29 13:15:50 1998 +0100
     1.2 +++ b/src/Pure/Syntax/token_trans.ML	Sun Nov 29 13:16:47 1998 +0100
     1.3 @@ -103,7 +103,7 @@
     1.4  
     1.5  (** emacs output (Isamode) **)
     1.6  
     1.7 -(* tags *)
     1.8 +local
     1.9  
    1.10  val end_tag = "\^A0";
    1.11  val tclass_tag = "\^A1";
    1.12 @@ -115,8 +115,7 @@
    1.13  
    1.14  fun tagit p x = (p ^ x ^ end_tag, size x);
    1.15  
    1.16 -
    1.17 -(* print mode "emacs" *)
    1.18 +in
    1.19  
    1.20  val emacs_trans =
    1.21   trans_mode "emacs"
    1.22 @@ -127,6 +126,37 @@
    1.23     ("bound", tagit bound_tag),
    1.24     ("var", tagit var_tag)];
    1.25  
    1.26 +end;
    1.27 +
    1.28 +
    1.29 +
    1.30 +(** ProofGeneral output **)
    1.31 +
    1.32 +local
    1.33 +
    1.34 +val end_tag = oct_char "350";
    1.35 +val tclass_tag = oct_char "351";
    1.36 +val tfree_tag = oct_char "352";
    1.37 +val tvar_tag = oct_char "353";
    1.38 +val free_tag = oct_char "354";
    1.39 +val bound_tag = oct_char "355";
    1.40 +val var_tag = oct_char "356";
    1.41 +
    1.42 +fun tagit p x = (p ^ x ^ end_tag, size x);
    1.43 +
    1.44 +in
    1.45 +
    1.46 +val proof_general_trans =
    1.47 + trans_mode "ProofGeneral"
    1.48 +  [("class", tagit tclass_tag),
    1.49 +   ("tfree", tagit tfree_tag),
    1.50 +   ("tvar", tagit tvar_tag),
    1.51 +   ("free", tagit free_tag),
    1.52 +   ("bound", tagit bound_tag),
    1.53 +   ("var", tagit var_tag)];
    1.54 +
    1.55 +end;
    1.56 +
    1.57  
    1.58  
    1.59  (** LaTeX output **)
    1.60 @@ -144,6 +174,7 @@
    1.61    map (fn s => ("", s, fn x => (x, size x))) std_token_classes @
    1.62    xterm_trans @
    1.63    emacs_trans @
    1.64 +  proof_general_trans @
    1.65    latex_trans;
    1.66  
    1.67