simplified pretty token metric: type int;
separate print_mode setup for Output/Pretty;

--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Jul 07 00:15:02 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Jul 07 00:15:02 2007 +0200
@@ -37,14 +37,14 @@
 fun xsymbols_output s =
   if print_mode_active Symbol.xsymbolsN andalso exists_string (equal "\\") s then
     let val syms = Symbol.explode s
-    in (implode (map xsym_output syms), real (Symbol.length syms)) end
-  else Symbol.default_output s;
+    in (implode (map xsym_output syms), Symbol.length syms) end
+  else Output.default_output s;
 
 in
 
 fun setup_xsymbols_output () =
-  Output.add_mode Symbol.xsymbolsN
-    (xsymbols_output, K xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
+  (Output.add_mode Symbol.xsymbolsN xsymbols_output Symbol.encode_raw;
+   Pretty.add_mode Symbol.xsymbolsN Pretty.default_indent Pretty.default_markup);
 
 end;
 
@@ -65,7 +65,7 @@
 fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
 
 fun tagit (kind, bg_tag) x =
-  (bg_tag () ^ x ^ end_tag (), real (Symbol.length (Symbol.explode x)));
+  (bg_tag () ^ x ^ end_tag (), Symbol.length (Symbol.explode x));
 
 fun free_or_skolem x =
   (case try Name.dest_skolem x of

--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Jul 07 00:15:02 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sat Jul 07 00:15:02 2007 +0200
@@ -50,13 +50,15 @@
 
 fun pgml_output str =
   let val syms = Symbol.explode str
-  in (implode (map pgml_sym syms), real (Symbol.length syms)) end;
+  in (implode (map pgml_sym syms), Symbol.length syms) end;
+
+fun pgml_markup (name, props) = ("", "");  (* FIXME *)
 
 in
 
 fun setup_proofgeneral_output () =
-  Output.add_mode proof_generalN
-    (pgml_output, K pgml_output, Symbol.default_indent, Symbol.encode_raw);
+  (Output.add_mode proof_generalN pgml_output Symbol.encode_raw;
+   Pretty.add_mode proof_generalN Pretty.default_indent pgml_markup);
 
 end;
 
@@ -76,7 +78,7 @@
 fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
 
 fun tagit kind x =
-  (xml_atom kind x, real (Symbol.length (Symbol.explode x)));
+  (xml_atom kind x, Symbol.length (Symbol.explode x));
 
 fun free_or_skolem x =
   (case try Name.dest_skolem x of

--- a/src/Pure/Thy/latex.ML	Sat Jul 07 00:15:02 2007 +0200
+++ b/src/Pure/Thy/latex.ML	Sat Jul 07 00:15:02 2007 +0200
@@ -165,14 +165,17 @@
 
 fun latex_output str =
   let val syms = Symbol.explode str
-  in (output_symbols syms, real (Symbol.length syms)) end;
-
-fun latex_keyword cmd =
-  apfst (enclose (if cmd then "\\isacommand{" else "\\isakeyword{") "}") o latex_output;
+  in (output_symbols syms, Symbol.length syms) end;
 
-fun latex_indent "" = ""
-  | latex_indent s = enclose "\\isaindent{" "}" s;
+fun latex_markup (s, _) =
+  if s = Markup.keywordN then ("\\isakeyword{", "}")
+  else if s = Markup.commandN then ("\\isacommand{", "}")
+  else ("", "");
 
-val _ = Output.add_mode latexN (latex_output, latex_keyword, latex_indent o #1, Symbol.encode_raw);
+fun latex_indent "" _ = ""
+  | latex_indent s _ = enclose "\\isaindent{" "}" s;
+
+val _ = Output.add_mode latexN latex_output Symbol.encode_raw;
+val _ = Pretty.add_mode latexN latex_indent latex_markup;
 
 end;