# HG changeset patch
# User berghofe
# Date 1106825649 -3600
# Node ID 4674102737e9b83c6c1ed5883abb334f4ee8040d
# Parent  e7f069887ec2f3f61e552284dc25c8473713d3dd
Added show_var_qmarks flag.

diff -r e7f069887ec2 -r 4674102737e9 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Wed Jan 26 17:34:42 2005 +0100
+++ b/src/Pure/proof_general.ML	Thu Jan 27 12:34:09 2005 +0100
@@ -581,7 +581,10 @@
        nat_option ProofContext.prems_limit)),
      ("print-depth", 
       ("Setting for the ML print depth",
-       print_depth_option))]),
+       print_depth_option)),
+     ("show-var-qmarks",
+      ("Show leading question mark of variable name",
+       bool_option show_var_qmarks))]),
    ("Tracing",
     [("trace-simplifier", 
       ("Trace simplification rules.",
diff -r e7f069887ec2 -r 4674102737e9 src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Jan 26 17:34:42 2005 +0100
+++ b/src/Pure/term.ML	Thu Jan 27 12:34:09 2005 +0100
@@ -164,6 +164,7 @@
   val exists_subterm: (term -> bool) -> term -> bool
   val compress_type: typ -> typ
   val compress_term: term -> term
+  val show_var_qmarks: bool ref
 end;
 
 signature TERM =
@@ -1088,14 +1089,17 @@
 
 (* string_of_vname *)
 
+val show_var_qmarks = ref true;
+
 fun string_of_vname (x, i) =
   let
     val si = string_of_int i;
     val dot = if_none (try (Symbol.is_digit o last_elem o Symbol.explode) x) true;
+    val qmark = if !show_var_qmarks then "?" else "";
   in
-    if dot then "?" ^ x ^ "." ^ si
-    else if i = 0 then "?" ^ x
-    else "?" ^ x ^ si
+    if dot then qmark ^ x ^ "." ^ si
+    else if i = 0 then qmark ^ x
+    else qmark ^ x ^ si
   end;
 
 fun string_of_vname' (x, ~1) = x