# HG changeset patch
# User wenzelm
# Date 912341807 -3600
# Node ID 9670dae0143d198a914d71c65d9ddf46e8409ce8
# Parent  1a2285f3db47e85a7554945b081c8cb070ef78e9
proof_general_trans (experimental);

diff -r 1a2285f3db47 -r 9670dae0143d src/Pure/Syntax/token_trans.ML
--- a/src/Pure/Syntax/token_trans.ML	Sun Nov 29 13:15:50 1998 +0100
+++ b/src/Pure/Syntax/token_trans.ML	Sun Nov 29 13:16:47 1998 +0100
@@ -103,7 +103,7 @@
 
 (** emacs output (Isamode) **)
 
-(* tags *)
+local
 
 val end_tag = "\^A0";
 val tclass_tag = "\^A1";
@@ -115,8 +115,7 @@
 
 fun tagit p x = (p ^ x ^ end_tag, size x);
 
-
-(* print mode "emacs" *)
+in
 
 val emacs_trans =
  trans_mode "emacs"
@@ -127,6 +126,37 @@
    ("bound", tagit bound_tag),
    ("var", tagit var_tag)];
 
+end;
+
+
+
+(** ProofGeneral output **)
+
+local
+
+val end_tag = oct_char "350";
+val tclass_tag = oct_char "351";
+val tfree_tag = oct_char "352";
+val tvar_tag = oct_char "353";
+val free_tag = oct_char "354";
+val bound_tag = oct_char "355";
+val var_tag = oct_char "356";
+
+fun tagit p x = (p ^ x ^ end_tag, size x);
+
+in
+
+val proof_general_trans =
+ trans_mode "ProofGeneral"
+  [("class", tagit tclass_tag),
+   ("tfree", tagit tfree_tag),
+   ("tvar", tagit tvar_tag),
+   ("free", tagit free_tag),
+   ("bound", tagit bound_tag),
+   ("var", tagit var_tag)];
+
+end;
+
 
 
 (** LaTeX output **)
@@ -144,6 +174,7 @@
   map (fn s => ("", s, fn x => (x, size x))) std_token_classes @
   xterm_trans @
   emacs_trans @
+  proof_general_trans @
   latex_trans;