src/Pure/term.ML
changeset 15986 db3cd4fa9b19
parent 15962 a3288211965a
child 16035 31bd65f7b22a
     1.1 --- a/src/Pure/term.ML	Tue May 17 18:10:38 2005 +0200
     1.2 +++ b/src/Pure/term.ML	Tue May 17 18:10:39 2005 +0200
     1.3 @@ -168,7 +168,7 @@
     1.4    val exists_subterm: (term -> bool) -> term -> bool
     1.5    val compress_type: typ -> typ
     1.6    val compress_term: term -> term
     1.7 -  val show_var_qmarks: bool ref
     1.8 +  val show_question_marks: bool ref
     1.9  end;
    1.10  
    1.11  signature TERM =
    1.12 @@ -1117,17 +1117,22 @@
    1.13  
    1.14  (* string_of_vname *)
    1.15  
    1.16 -val show_var_qmarks = ref true;
    1.17 +val show_question_marks = ref true;
    1.18  
    1.19  fun string_of_vname (x, i) =
    1.20    let
    1.21 -    val si = string_of_int i;
    1.22 -    val dot = getOpt (try (Symbol.is_digit o List.last o Symbol.explode) x, true);
    1.23 -    val qmark = if !show_var_qmarks then "?" else "";
    1.24 +    val question_mark = if ! show_question_marks then "?" else "";
    1.25 +    val idx = string_of_int i;
    1.26 +    val dot =
    1.27 +      (case rev (Symbol.explode x) of
    1.28 +        _ :: "\\<^isub>" :: _ => false
    1.29 +      | _ :: "\\<^isup>" :: _ => false
    1.30 +      | c :: _ => Symbol.is_digit c
    1.31 +      | _ => true);
    1.32    in
    1.33 -    if dot then qmark ^ x ^ "." ^ si
    1.34 -    else if i = 0 then qmark ^ x
    1.35 -    else qmark ^ x ^ si
    1.36 +    if dot then question_mark ^ x ^ "." ^ idx
    1.37 +    else if i <> 0 then question_mark ^ x ^ idx
    1.38 +    else question_mark ^ x
    1.39    end;
    1.40  
    1.41  fun string_of_vname' (x, ~1) = x