explicit option skip_proofs;
authorwenzelm
Wed Aug 01 15:46:45 2012 +0200 (2012-08-01)
changeset 4863430a6e841390a
parent 48633 7cd32f9d4293
child 48635 bfce940c6f38
explicit option skip_proofs;
etc/options
src/Pure/ProofGeneral/preferences.ML
src/Pure/System/build.ML
     1.1 --- a/etc/options	Wed Aug 01 15:33:08 2012 +0200
     1.2 +++ b/etc/options	Wed Aug 01 15:46:45 2012 +0200
     1.3 @@ -30,6 +30,8 @@
     1.4    -- "level of detail for proof objects: 0, 1, 2"
     1.5  declare quick_and_dirty : bool = false
     1.6    -- "if true then some tools will OMIT some proofs"
     1.7 +declare skip_proofs : bool = false
     1.8 +  -- "skip over proofs"
     1.9  
    1.10  declare condition : string = ""
    1.11    -- "required environment variables for subsequent theories (separated by commas)"
     2.1 --- a/src/Pure/ProofGeneral/preferences.ML	Wed Aug 01 15:33:08 2012 +0200
     2.2 +++ b/src/Pure/ProofGeneral/preferences.ML	Wed Aug 01 15:46:45 2012 +0200
     2.3 @@ -171,7 +171,7 @@
     2.4        "Take a few short cuts") (),
     2.5    bool_pref Toplevel.skip_proofs
     2.6      "skip-proofs"
     2.7 -    "Skip over proofs (interactive-only)",
     2.8 +    "Skip over proofs",
     2.9    proof_pref,
    2.10    nat_pref Multithreading.max_threads
    2.11      "max-threads"
     3.1 --- a/src/Pure/System/build.ML	Wed Aug 01 15:33:08 2012 +0200
     3.2 +++ b/src/Pure/System/build.ML	Wed Aug 01 15:46:45 2012 +0200
     3.3 @@ -30,6 +30,7 @@
     3.4      |> Unsynchronized.setmp Multithreading.max_threads (Options.int options "threads")
     3.5      |> no_document options ? Present.no_document
     3.6      |> Unsynchronized.setmp quick_and_dirty (Options.bool options "quick_and_dirty")
     3.7 +    |> Unsynchronized.setmp Toplevel.skip_proofs (Options.bool options "skip_proofs")
     3.8      |> Unsynchronized.setmp Printer.show_question_marks_default
     3.9          (Options.bool options "show_question_marks")
    3.10      |> Unsynchronized.setmp Name_Space.names_long_default (Options.bool options "names_long")