src/Pure/Thy/thy_output.ML
changeset 27882 eaa9fef9f4c1
parent 27874 f0364f1c0ecf
child 27897 0e7ff439460f
--- a/src/Pure/Thy/thy_output.ML	Thu Aug 14 21:06:07 2008 +0200
+++ b/src/Pure/Thy/thy_output.ML	Fri Aug 15 15:50:44 2008 +0200
@@ -508,7 +508,7 @@
 
 fun output_ml ml src ctxt (txt, pos) =
  (ML_Context.eval_in (SOME (Context.Proof ctxt)) false pos (ml txt);
-  (if ! source then str_of_source src else txt)
+  (if ! source then str_of_source src else SymbolPos.content (SymbolPos.explode (txt, pos)))
   |> (if ! quotes then quote else I)
   |> (if ! display then enclose "\\begin{verbatim}\n" "\n\\end{verbatim}"
   else
@@ -545,7 +545,7 @@
   ("term_type", args Args.term (output pretty_term_typ)),
   ("typeof", args Args.term (output pretty_term_typeof)),
   ("const", args Args.const_proper (output pretty_const)),
-  ("abbrev", args (Scan.lift Args.name) (output pretty_abbrev)),
+  ("abbrev", args (Scan.lift Args.name_source) (output pretty_abbrev)),
   ("typ", args Args.typ_abbrev (output Syntax.pretty_typ)),
   ("text", args (Scan.lift Args.name) (output (K pretty_text))),
   ("goals", output_goals true),
@@ -553,8 +553,8 @@
   ("prf", args Attrib.thms (output (pretty_prf false))),
   ("full_prf", args Attrib.thms (output (pretty_prf true))),
   ("theory", args (Scan.lift Args.name) (output pretty_theory)),
-  ("ML", args (Scan.lift (P.position Args.name)) (output_ml ml_val)),
-  ("ML_type", args (Scan.lift (P.position Args.name)) (output_ml ml_type)),
-  ("ML_struct", args (Scan.lift (P.position Args.name)) (output_ml ml_struct))];
+  ("ML", args (Scan.lift Args.name_source_position) (output_ml ml_val)),
+  ("ML_type", args (Scan.lift Args.name_source_position) (output_ml ml_type)),
+  ("ML_struct", args (Scan.lift Args.name_source_position) (output_ml ml_struct))];
 
 end;