turned show_question_marks into proper configuration option;
authorwenzelm
Thu Sep 02 00:48:07 2010 +0200 (2010-09-02)
changeset 38980af73cf0dc31f
parent 38979 60dbf0b3f6c7
child 39040 e3799716b733
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
tuned;
NEWS
doc-src/IsarRef/Thy/Inner_Syntax.thy
doc-src/IsarRef/Thy/document/Inner_Syntax.tex
doc-src/LaTeXsugar/Sugar/Sugar.thy
doc-src/LaTeXsugar/Sugar/document/Sugar.tex
src/Pure/Isar/attrib.ML
src/Pure/Isar/proof_context.ML
src/Pure/ProofGeneral/preferences.ML
src/Pure/Syntax/printer.ML
src/Pure/Thy/thy_output.ML
src/Pure/term.ML
src/Tools/WWW_Find/find_theorems.ML
     1.1 --- a/NEWS	Wed Sep 01 23:43:45 2010 +0200
     1.2 +++ b/NEWS	Thu Sep 02 00:48:07 2010 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4  at the cost of clarity of file dependencies.  Recall that Isabelle/ML
     1.5  files exclusively use the .ML extension.  Minor INCOMPATIBILTY.
     1.6  
     1.7 -* Various options that affect document antiquotations are now properly
     1.8 +* Various options that affect pretty printing etc. are now properly
     1.9  handled within the context via configuration options, instead of
    1.10  unsynchronized references.  There are both ML Config.T entities and
    1.11  Isar declaration attributes to access these.
    1.12 @@ -36,15 +36,11 @@
    1.13    Thy_Output.source         thy_output_source
    1.14    Thy_Output.break          thy_output_break
    1.15  
    1.16 +  show_question_marks       show_question_marks
    1.17 +
    1.18  Note that the corresponding "..._default" references may be only
    1.19  changed globally at the ROOT session setup, but *not* within a theory.
    1.20  
    1.21 -* ML structure Unsynchronized never opened, not even in Isar
    1.22 -interaction mode as before.  Old Unsynchronized.set etc. have been
    1.23 -discontinued -- use plain := instead.  This should be *rare* anyway,
    1.24 -since modern tools always work via official context data, notably
    1.25 -configuration options.
    1.26 -
    1.27  
    1.28  *** Pure ***
    1.29  
    1.30 @@ -217,6 +213,15 @@
    1.31  
    1.32  *** ML ***
    1.33  
    1.34 +* Configuration option show_question_marks only affects regular pretty
    1.35 +printing of types and terms, not raw Term.string_of_vname.
    1.36 +
    1.37 +* ML structure Unsynchronized never opened, not even in Isar
    1.38 +interaction mode as before.  Old Unsynchronized.set etc. have been
    1.39 +discontinued -- use plain := instead.  This should be *rare* anyway,
    1.40 +since modern tools always work via official context data, notably
    1.41 +configuration options.
    1.42 +
    1.43  * ML antiquotations @{theory} and @{theory_ref} refer to named
    1.44  theories from the ancestry of the current context, not any accidental
    1.45  theory loader state as before.  Potential INCOMPATIBILITY, subtle
     2.1 --- a/doc-src/IsarRef/Thy/Inner_Syntax.thy	Wed Sep 01 23:43:45 2010 +0200
     2.2 +++ b/doc-src/IsarRef/Thy/Inner_Syntax.thy	Thu Sep 02 00:48:07 2010 +0200
     2.3 @@ -108,7 +108,7 @@
     2.4      @{index_ML Proof.show_main_goal: "bool Unsynchronized.ref"} & default @{ML false} \\
     2.5      @{index_ML show_hyps: "bool Unsynchronized.ref"} & default @{ML false} \\
     2.6      @{index_ML show_tags: "bool Unsynchronized.ref"} & default @{ML false} \\
     2.7 -    @{index_ML show_question_marks: "bool Unsynchronized.ref"} & default @{ML true} \\
     2.8 +    @{index_ML show_question_marks: "bool Config.T"} & default @{ML true} \\
     2.9    \end{mldecls}
    2.10  
    2.11    These global ML variables control the detail of information that is
     3.1 --- a/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Wed Sep 01 23:43:45 2010 +0200
     3.2 +++ b/doc-src/IsarRef/Thy/document/Inner_Syntax.tex	Thu Sep 02 00:48:07 2010 +0200
     3.3 @@ -130,7 +130,7 @@
     3.4      \indexdef{}{ML}{Proof.show\_main\_goal}\verb|Proof.show_main_goal: bool Unsynchronized.ref| & default \verb|false| \\
     3.5      \indexdef{}{ML}{show\_hyps}\verb|show_hyps: bool Unsynchronized.ref| & default \verb|false| \\
     3.6      \indexdef{}{ML}{show\_tags}\verb|show_tags: bool Unsynchronized.ref| & default \verb|false| \\
     3.7 -    \indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool Unsynchronized.ref| & default \verb|true| \\
     3.8 +    \indexdef{}{ML}{show\_question\_marks}\verb|show_question_marks: bool Config.T| & default \verb|true| \\
     3.9    \end{mldecls}
    3.10  
    3.11    These global ML variables control the detail of information that is
     4.1 --- a/doc-src/LaTeXsugar/Sugar/Sugar.thy	Wed Sep 01 23:43:45 2010 +0200
     4.2 +++ b/doc-src/LaTeXsugar/Sugar/Sugar.thy	Thu Sep 02 00:48:07 2010 +0200
     4.3 @@ -132,19 +132,19 @@
     4.4  This \verb!no_vars! business can become a bit tedious.
     4.5  If you would rather never see question marks, simply put
     4.6  \begin{quote}
     4.7 -@{ML "show_question_marks := false"}\verb!;!
     4.8 +@{ML "show_question_marks_default := false"}\verb!;!
     4.9  \end{quote}
    4.10  at the beginning of your file \texttt{ROOT.ML}.
    4.11  The rest of this document is produced with this flag set to \texttt{false}.
    4.12  
    4.13 -Hint: Setting \verb!show_question_marks! to \texttt{false} only
    4.14 +Hint: Setting \verb!show_question_marks_default! to \texttt{false} only
    4.15  suppresses question marks; variables that end in digits,
    4.16  e.g. @{text"x1"}, are still printed with a trailing @{text".0"},
    4.17  e.g. @{text"x1.0"}, their internal index. This can be avoided by
    4.18  turning the last digit into a subscript: write \verb!x\<^isub>1! and
    4.19  obtain the much nicer @{text"x\<^isub>1"}. *}
    4.20  
    4.21 -(*<*)ML "show_question_marks := false"(*>*)
    4.22 +(*<*)declare [[show_question_marks = false]](*>*)
    4.23  
    4.24  subsection {*Qualified names*}
    4.25  
     5.1 --- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Wed Sep 01 23:43:45 2010 +0200
     5.2 +++ b/doc-src/LaTeXsugar/Sugar/document/Sugar.tex	Thu Sep 02 00:48:07 2010 +0200
     5.3 @@ -164,7 +164,7 @@
     5.4  \begin{isamarkuptext}%
     5.5  If you print anything, especially theorems, containing
     5.6  schematic variables they are prefixed with a question mark:
     5.7 -\verb!@!\verb!{thm conjI}! results in \isa{{\isasymlbrakk}P{\isacharsemicolon}\ Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isasymand}\ Q}. Most of the time
     5.8 +\verb!@!\verb!{thm conjI}! results in \isa{{\isasymlbrakk}{\isacharquery}P{\isacharsemicolon}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isasymand}\ {\isacharquery}Q}. Most of the time
     5.9  you would rather not see the question marks. There is an attribute
    5.10  \verb!no_vars! that you can attach to the theorem that turns its
    5.11  schematic into ordinary free variables: \verb!@!\verb!{thm conjI[no_vars]}!
    5.12 @@ -173,12 +173,12 @@
    5.13  This \verb!no_vars! business can become a bit tedious.
    5.14  If you would rather never see question marks, simply put
    5.15  \begin{quote}
    5.16 -\verb|show_question_marks := false|\verb!;!
    5.17 +\verb|show_question_marks_default := false|\verb!;!
    5.18  \end{quote}
    5.19  at the beginning of your file \texttt{ROOT.ML}.
    5.20  The rest of this document is produced with this flag set to \texttt{false}.
    5.21  
    5.22 -Hint: Setting \verb!show_question_marks! to \texttt{false} only
    5.23 +Hint: Setting \verb!show_question_marks_default! to \texttt{false} only
    5.24  suppresses question marks; variables that end in digits,
    5.25  e.g. \isa{x{\isadigit{1}}}, are still printed with a trailing \isa{{\isachardot}{\isadigit{0}}},
    5.26  e.g. \isa{x{\isadigit{1}}{\isachardot}{\isadigit{0}}}, their internal index. This can be avoided by
    5.27 @@ -187,19 +187,6 @@
    5.28  \end{isamarkuptext}%
    5.29  \isamarkuptrue%
    5.30  %
    5.31 -\isadelimML
    5.32 -%
    5.33 -\endisadelimML
    5.34 -%
    5.35 -\isatagML
    5.36 -%
    5.37 -\endisatagML
    5.38 -{\isafoldML}%
    5.39 -%
    5.40 -\isadelimML
    5.41 -%
    5.42 -\endisadelimML
    5.43 -%
    5.44  \isamarkupsubsection{Qualified names%
    5.45  }
    5.46  \isamarkuptrue%
     6.1 --- a/src/Pure/Isar/attrib.ML	Wed Sep 01 23:43:45 2010 +0200
     6.2 +++ b/src/Pure/Isar/attrib.ML	Thu Sep 02 00:48:07 2010 +0200
     6.3 @@ -392,7 +392,8 @@
     6.4  (* theory setup *)
     6.5  
     6.6  val _ = Context.>> (Context.map_theory
     6.7 - (register_config Unify.trace_bound_value #>
     6.8 + (register_config show_question_marks_value #>
     6.9 +  register_config Unify.trace_bound_value #>
    6.10    register_config Unify.search_bound_value #>
    6.11    register_config Unify.trace_simp_value #>
    6.12    register_config Unify.trace_types_value #>
     7.1 --- a/src/Pure/Isar/proof_context.ML	Wed Sep 01 23:43:45 2010 +0200
     7.2 +++ b/src/Pure/Isar/proof_context.ML	Thu Sep 02 00:48:07 2010 +0200
     7.3 @@ -413,8 +413,7 @@
     7.4      SOME (x, i) =>
     7.5        (case try Name.dest_skolem x of
     7.6          NONE => Pretty.mark Markup.var (Pretty.str s)
     7.7 -      | SOME x' => Pretty.mark Markup.skolem
     7.8 -          (Pretty.str (setmp_CRITICAL show_question_marks true Term.string_of_vname (x', i))))
     7.9 +      | SOME x' => Pretty.mark Markup.skolem (Pretty.str (Term.string_of_vname (x', i))))
    7.10    | NONE => Pretty.mark Markup.var (Pretty.str s));
    7.11  
    7.12  fun plain_markup m _ s = Pretty.mark m (Pretty.str s);
     8.1 --- a/src/Pure/ProofGeneral/preferences.ML	Wed Sep 01 23:43:45 2010 +0200
     8.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Thu Sep 02 00:48:07 2010 +0200
     8.3 @@ -141,7 +141,7 @@
     8.4      "prems-limit"
     8.5      "Setting for maximum number of premises printed",
     8.6    print_depth_pref,
     8.7 -  bool_pref show_question_marks
     8.8 +  bool_pref show_question_marks_default
     8.9      "show-question-marks"
    8.10      "Show leading question mark of variable name"];
    8.11  
     9.1 --- a/src/Pure/Syntax/printer.ML	Wed Sep 01 23:43:45 2010 +0200
     9.2 +++ b/src/Pure/Syntax/printer.ML	Thu Sep 02 00:48:07 2010 +0200
     9.3 @@ -12,6 +12,9 @@
     9.4    val show_no_free_types: bool Unsynchronized.ref
     9.5    val show_all_types: bool Unsynchronized.ref
     9.6    val show_structs: bool Unsynchronized.ref
     9.7 +  val show_question_marks_default: bool Unsynchronized.ref
     9.8 +  val show_question_marks_value: Config.value Config.T
     9.9 +  val show_question_marks: bool Config.T
    9.10    val pp_show_brackets: Pretty.pp -> Pretty.pp
    9.11  end;
    9.12  
    9.13 @@ -52,6 +55,11 @@
    9.14  val show_all_types = Unsynchronized.ref false;
    9.15  val show_structs = Unsynchronized.ref false;
    9.16  
    9.17 +val show_question_marks_default = Unsynchronized.ref true;
    9.18 +val show_question_marks_value =
    9.19 +  Config.declare false "show_question_marks" (fn _ => Config.Bool (! show_question_marks_default));
    9.20 +val show_question_marks = Config.bool show_question_marks_value;
    9.21 +
    9.22  fun pp_show_brackets pp = Pretty.pp (setmp_CRITICAL show_brackets true (Pretty.term pp),
    9.23    Pretty.typ pp, Pretty.sort pp, Pretty.classrel pp, Pretty.arity pp);
    9.24  
    9.25 @@ -72,15 +80,18 @@
    9.26  
    9.27  (* simple_ast_of *)
    9.28  
    9.29 -fun simple_ast_of (Const (c, _)) = Ast.Constant c
    9.30 -  | simple_ast_of (Free (x, _)) = Ast.Variable x
    9.31 -  | simple_ast_of (Var (xi, _)) = Ast.Variable (Term.string_of_vname xi)
    9.32 -  | simple_ast_of (t as _ $ _) =
    9.33 -      let val (f, args) = strip_comb t in
    9.34 -        Ast.mk_appl (simple_ast_of f) (map simple_ast_of args)
    9.35 -      end
    9.36 -  | simple_ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i)
    9.37 -  | simple_ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
    9.38 +fun simple_ast_of ctxt =
    9.39 +  let
    9.40 +    val tune_var = if Config.get ctxt show_question_marks then I else unprefix "?";
    9.41 +    fun ast_of (Const (c, _)) = Ast.Constant c
    9.42 +      | ast_of (Free (x, _)) = Ast.Variable x
    9.43 +      | ast_of (Var (xi, _)) = Ast.Variable (tune_var (Term.string_of_vname xi))
    9.44 +      | ast_of (t as _ $ _) =
    9.45 +          let val (f, args) = strip_comb t
    9.46 +          in Ast.mk_appl (ast_of f) (map ast_of args) end
    9.47 +      | ast_of (Bound i) = Ast.Variable ("B." ^ string_of_int i)
    9.48 +      | ast_of (Abs _) = raise Fail "simple_ast_of: Abs";
    9.49 +  in ast_of end;
    9.50  
    9.51  
    9.52  
    9.53 @@ -88,14 +99,14 @@
    9.54  
    9.55  fun ast_of_termT ctxt trf tm =
    9.56    let
    9.57 -    fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of t
    9.58 -      | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of t
    9.59 +    fun ast_of (t as Const ("_tfree", _) $ Free _) = simple_ast_of ctxt t
    9.60 +      | ast_of (t as Const ("_tvar", _) $ Var _) = simple_ast_of ctxt t
    9.61        | ast_of (Const (a, _)) = trans a []
    9.62        | ast_of (t as _ $ _) =
    9.63            (case strip_comb t of
    9.64              (Const (a, _), args) => trans a args
    9.65            | (f, args) => Ast.Appl (map ast_of (f :: args)))
    9.66 -      | ast_of t = simple_ast_of t
    9.67 +      | ast_of t = simple_ast_of ctxt t
    9.68      and trans a args =
    9.69        ast_of (apply_trans ctxt (apply_typed false dummyT (trf a)) args)
    9.70          handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args);
    9.71 @@ -168,7 +179,7 @@
    9.72            if show_all_types
    9.73            then Ast.mk_appl (constrain const T) (map ast_of ts)
    9.74            else trans c T ts
    9.75 -      | (t, ts) => Ast.mk_appl (simple_ast_of t) (map ast_of ts))
    9.76 +      | (t, ts) => Ast.mk_appl (simple_ast_of ctxt t) (map ast_of ts))
    9.77  
    9.78      and trans a T args =
    9.79        ast_of (apply_trans ctxt (apply_typed show_sorts T (trf a)) args)
    9.80 @@ -176,9 +187,9 @@
    9.81  
    9.82      and constrain t T =
    9.83        if show_types andalso T <> dummyT then
    9.84 -        Ast.Appl [Ast.Constant Syn_Ext.constrainC, simple_ast_of t,
    9.85 +        Ast.Appl [Ast.Constant Syn_Ext.constrainC, simple_ast_of ctxt t,
    9.86            ast_of_termT ctxt trf (Type_Ext.term_of_typ show_sorts T)]
    9.87 -      else simple_ast_of t;
    9.88 +      else simple_ast_of ctxt t;
    9.89    in
    9.90      tm
    9.91      |> Syn_Trans.prop_tr'
    10.1 --- a/src/Pure/Thy/thy_output.ML	Wed Sep 01 23:43:45 2010 +0200
    10.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Sep 02 00:48:07 2010 +0200
    10.3 @@ -447,7 +447,7 @@
    10.4  val _ = add_option "show_types" (add_wrapper o setmp_CRITICAL Syntax.show_types o boolean);
    10.5  val _ = add_option "show_sorts" (add_wrapper o setmp_CRITICAL Syntax.show_sorts o boolean);
    10.6  val _ = add_option "show_structs" (add_wrapper o setmp_CRITICAL show_structs o boolean);
    10.7 -val _ = add_option "show_question_marks" (add_wrapper o setmp_CRITICAL show_question_marks o boolean);
    10.8 +val _ = add_option "show_question_marks" (Config.put show_question_marks o boolean);
    10.9  val _ = add_option "long_names" (add_wrapper o setmp_CRITICAL Name_Space.long_names o boolean);
   10.10  val _ = add_option "short_names" (add_wrapper o setmp_CRITICAL Name_Space.short_names o boolean);
   10.11  val _ = add_option "unique_names" (add_wrapper o setmp_CRITICAL Name_Space.unique_names o boolean);
    11.1 --- a/src/Pure/term.ML	Wed Sep 01 23:43:45 2010 +0200
    11.2 +++ b/src/Pure/term.ML	Thu Sep 02 00:48:07 2010 +0200
    11.3 @@ -114,7 +114,6 @@
    11.4    val exists_type: (typ -> bool) -> term -> bool
    11.5    val exists_subterm: (term -> bool) -> term -> bool
    11.6    val exists_Const: (string * typ -> bool) -> term -> bool
    11.7 -  val show_question_marks: bool Unsynchronized.ref
    11.8  end;
    11.9  
   11.10  signature TERM =
   11.11 @@ -983,11 +982,8 @@
   11.12  
   11.13  (* display variables *)
   11.14  
   11.15 -val show_question_marks = Unsynchronized.ref true;
   11.16 -
   11.17  fun string_of_vname (x, i) =
   11.18    let
   11.19 -    val question_mark = if ! show_question_marks then "?" else "";
   11.20      val idx = string_of_int i;
   11.21      val dot =
   11.22        (case rev (Symbol.explode x) of
   11.23 @@ -996,9 +992,9 @@
   11.24        | c :: _ => Symbol.is_digit c
   11.25        | _ => true);
   11.26    in
   11.27 -    if dot then question_mark ^ x ^ "." ^ idx
   11.28 -    else if i <> 0 then question_mark ^ x ^ idx
   11.29 -    else question_mark ^ x
   11.30 +    if dot then "?" ^ x ^ "." ^ idx
   11.31 +    else if i <> 0 then "?" ^ x ^ idx
   11.32 +    else "?" ^ x
   11.33    end;
   11.34  
   11.35  fun string_of_vname' (x, ~1) = x
    12.1 --- a/src/Tools/WWW_Find/find_theorems.ML	Wed Sep 01 23:43:45 2010 +0200
    12.2 +++ b/src/Tools/WWW_Find/find_theorems.ML	Thu Sep 02 00:48:07 2010 +0200
    12.3 @@ -143,9 +143,9 @@
    12.4  
    12.5  fun html_thm ctxt (n, (thmref, thm)) =
    12.6    let
    12.7 -    val string_of_thm =
    12.8 +    val output_thm =
    12.9        Output.output o Pretty.string_of_margin 100 o
   12.10 -        setmp_CRITICAL show_question_marks false (Display.pretty_thm ctxt);
   12.11 +        Display.pretty_thm (Config.put show_question_marks false ctxt);
   12.12    in
   12.13      tag' "tr" (class ("row" ^ Int.toString (n mod 2)))
   12.14        [
   12.15 @@ -153,7 +153,7 @@
   12.16            [span' (sorry_class thm)
   12.17               [raw_text (Facts.string_of_ref thmref)]
   12.18            ],
   12.19 -        tag' "td" (class "thm") [pre noid (string_of_thm thm)]
   12.20 +        tag' "td" (class "thm") [pre noid (output_thm thm)]
   12.21        ]
   12.22    end;
   12.23  
   12.24 @@ -236,7 +236,7 @@
   12.25    end;
   12.26  in
   12.27  
   12.28 -val () = show_question_marks := false;
   12.29 +val () = show_question_marks_default := false;
   12.30  val () = ScgiServer.register (find_theorems_url, SOME Mime.html, find_theorems);
   12.31  
   12.32  end;