# HG changeset patch # User aspinall # Date 1172922966 -3600 # Node ID 3878265f4924434071499f4cbe6c6e9e55e41304 # Parent 6e52564bcb536bfca4bc2d0f8ec90e8006221e8d Simplify print mode. Support setproverflag. diff -r 6e52564bcb53 -r 3878265f4924 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Sat Mar 03 12:43:16 2007 +0100 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Sat Mar 03 12:56:06 2007 +0100 @@ -28,33 +28,25 @@ open Pgip; -(* print modes *) +(* print mode *) -val proof_generalN = "ProofGeneral"; (*token markup (colouring vars, etc.)*) -val pgmlN = "PGML"; (*XML escapes and PGML symbol elements*) -val thm_depsN = "thm_deps"; (*meta-information about theorem deps*) - - -(* text output: print modes for xsymbol and PGML *) +val proof_generalN = "ProofGeneral"; +val pgmlsymbols_flag = ref true; local fun xsym_output "\\" = "\\\\" | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s; -fun xsymbols_output s = - if Output.has_mode Symbol.xsymbolsN andalso exists_string (equal "\\") s then - let val syms = Symbol.explode s - in (implode (map xsym_output syms), real (Symbol.length syms)) end - else Symbol.default_output s; - -(* XML immediately rendered pretty printer. Take care not to double escape *) fun pgml_sym s = (case Symbol.decode s of Symbol.Char s => XML.text s - | Symbol.Sym sn => XML.element "sym" [("name", sn)] [XML.text s] - | Symbol.Ctrl sn => XML.element "ctrl" [("name", sn)] [XML.text s] (* FIXME: no such PGML! *) - | Symbol.Raw rs => rs); + | Symbol.Sym sn => + let val ascii = implode (map xsym_output (Symbol.explode s)) + in if !pgmlsymbols_flag then XML.element "sym" [("name", sn)] [XML.text ascii] + else ascii end + | Symbol.Ctrl sn => XML.element "ctrl" [("name", sn)] [XML.text sn] (* FIXME: no such PGML *) + | Symbol.Raw raw => raw); fun pgml_output str = let val syms = Symbol.explode str @@ -62,12 +54,8 @@ in -fun setup_xsymbols_output () = - Output.add_mode Symbol.xsymbolsN - (xsymbols_output, K xsymbols_output, Symbol.default_indent, Symbol.encode_raw); - -fun setup_pgml_output () = - Output.add_mode pgmlN +fun setup_proofgeneral_output () = + Output.add_mode proof_generalN (pgml_output, K pgml_output, Symbol.default_indent, Symbol.encode_raw); end; @@ -341,6 +329,9 @@ (* theorem dependency output *) + +val show_theorem_dependencies = ref false; + local val spaces_quote = space_implode " " o map quote; @@ -355,7 +346,7 @@ end fun tell_thm_deps ths = - if Output.has_mode thm_depsN then + if !show_theorem_dependencies then let val names = map PureThy.get_name_hint (filter PureThy.has_name_hint ths); val deps = (Symtab.keys (fold Proofterm.thms_of_proof' @@ -436,9 +427,10 @@ fun setup_preferences_tweak() = preferences := - (* PGIP uses markup for distinguishing variable types *) (!preferences |> Preferences.set_default ("show-question-marks","false") - |> Preferences.remove "show-question-marks"); + |> Preferences.remove "show-question-marks" (* we use markup, not ?s *) + |> Preferences.remove "theorem-dependencies" (* set internally *) + |> Preferences.remove "full-proofs") (* set internally *) @@ -528,16 +520,36 @@ fun proverexit vs = isarcmd "quit" -fun startquiet vs = isarcmd "disable_pr" +fun set_proverflag_quiet b = + isarcmd (if b then "disable_pr" else "enable_pr") -fun stopquiet vs = isarcmd "enable_pr" +fun set_proverflag_pgmlsymbols b = + (pgmlsymbols_flag := b; + change print_mode + (fn mode => + remove (op =) Symbol.xsymbolsN mode @ (if b then [Symbol.xsymbolsN] else []))) + +fun set_proverflag_thmdeps b = + (show_theorem_dependencies := b; + proofs := (if b then 1 else 2)) -fun pgmlsymbolson vs = - change print_mode (fn mode => - remove (op =) Symbol.xsymbolsN mode @ [Symbol.xsymbolsN]) +fun startquiet vs = set_proverflag_quiet true; (* TO BE REMOVED *) +fun stopquiet vs = set_proverflag_quiet false; (* TO BE REMOVED *) +fun pgmlsymbolson vs = set_proverflag_pgmlsymbols true; (* TO BE REMOVED *) +fun pgmlsymbolsoff vs = set_proverflag_pgmlsymbols false; (* TO BE REMOVED *) -fun pgmlsymbolsoff vs = - change print_mode (remove (op =) Symbol.xsymbolsN) +fun setproverflag (Setproverflag vs) = + let + val flagname = #flagname vs + val value = #value vs + in + (case flagname of + "quiet" => set_proverflag_quiet value + | "pgmlsymbols" => set_proverflag_pgmlsymbols value + | "metainfo:thmdeps" => set_proverflag_thmdeps value + | _ => log_msg ("Unrecognised prover control flag: " ^ (quote flagname) ^ " ignored.")) + end + fun dostep (Dostep vs) = let @@ -946,6 +958,7 @@ | Pgip.Stopquiet _ => stopquiet inp | Pgip.Pgmlsymbolson _ => pgmlsymbolson inp | Pgip.Pgmlsymbolsoff _ => pgmlsymbolsoff inp + | Pgip.Setproverflag _ => setproverflag inp | Pgip.Dostep _ => dostep inp | Pgip.Undostep _ => undostep inp | Pgip.Redostep _ => redostep inp @@ -1101,8 +1114,7 @@ (setmp warning_fn (K ()) init_outer_syntax (); PgipParser.init (); setup_preferences_tweak (); - setup_xsymbols_output (); - setup_pgml_output (); + setup_proofgeneral_output (); setup_messages (); setup_state (); setup_thy_loader (); @@ -1112,7 +1124,6 @@ set initialized); sync_thy_loader (); change print_mode (cons proof_generalN o remove (op =) proof_generalN); - change print_mode (append [pgmlN] o subtract (op =) [pgmlN]); pgip_toplevel tty_src);