# HG changeset patch # User wenzelm # Date 910622081 -3600 # Node ID 996361157cfbf6cc57929f035ee43cdfbfeb718c # Parent 95b619c7289ba21db7c272656f4e72ace360e61c Non-logical toplevel commands. diff -r 95b619c7289b -r 996361157cfb src/Pure/Isar/isar_cmd.ML --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Pure/Isar/isar_cmd.ML Mon Nov 09 15:34:41 1998 +0100 @@ -0,0 +1,141 @@ +(* Title: Pure/Isar/isar_cmd.ML + ID: $Id$ + Author: Markus Wenzel, TU Muenchen + +Non-logical toplevel commands. +*) + +signature ISAR_CMD = +sig + val break: Toplevel.transition -> Toplevel.transition + val exit: Toplevel.transition -> Toplevel.transition + val quit: Toplevel.transition -> Toplevel.transition + val use: string -> Toplevel.transition -> Toplevel.transition + val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition + val use_mltext: string -> Toplevel.transition -> Toplevel.transition + val use_commit: Toplevel.transition -> Toplevel.transition + val cd: string -> Toplevel.transition -> Toplevel.transition + val pwd: Toplevel.transition -> Toplevel.transition + val use_thy: string -> Toplevel.transition -> Toplevel.transition + val load: string -> Toplevel.transition -> Toplevel.transition + val print_theory: Toplevel.transition -> Toplevel.transition + val print_syntax: Toplevel.transition -> Toplevel.transition + val print_attributes: Toplevel.transition -> Toplevel.transition + val print_methods: Toplevel.transition -> Toplevel.transition + val print_binds: Toplevel.transition -> Toplevel.transition + val print_lthms: Toplevel.transition -> Toplevel.transition + val print_thms: xstring -> Toplevel.transition -> Toplevel.transition + val print_prop: string -> Toplevel.transition -> Toplevel.transition + val print_term: string -> Toplevel.transition -> Toplevel.transition + val print_type: string -> Toplevel.transition -> Toplevel.transition +end; + +structure IsarCmd: ISAR_CMD = +struct + + +(* variations on exit *) + +val break = Toplevel.imperative (fn () => raise Toplevel.BREAK); + +val exit = Toplevel.keep (fn state => + (Context.set_context (try Toplevel.theory_of state); + writeln "Leaving the Isar loop. Invoke 'main_loop();' to restart."; + raise Toplevel.TERMINATE)); + +val quit = Toplevel.imperative quit; + + +(* use ML text *) + +fun use name = Toplevel.imperative (fn () => Use.use name); + +(*passes changes of theory context*) +val use_mltext_theory = Toplevel.theory o IsarThy.use_mltext_theory; + +(*ignore result theory context*) +fun use_mltext txt = Toplevel.keep (fn state => + (IsarThy.use_mltext txt (try Toplevel.theory_of state); ())); + +(*Note: commit is dynamically bound*) +val use_commit = use_mltext "commit();"; + + +(* current working directory *) + +fun print_cd _ = writeln (Library.pwd ()); + +fun cd dir = Toplevel.imperative (fn () => (Use.cd dir; print_cd ())); +val pwd = Toplevel.imperative print_cd; + + +(* load theory files *) + +fun use_thy name = Toplevel.imperative (fn () => ThyRead.use_thy name); + +fun load name = + Toplevel.imperative (fn () => Toplevel.excursion (OuterSyntax.read_file (name ^ ".thy"))); + + +(* print theory contents *) + +val print_theory = Toplevel.keep (PureThy.print_theory o Toplevel.theory_of); +val print_syntax = Toplevel.keep (Display.print_syntax o Toplevel.theory_of); +val print_attributes = Toplevel.keep (Attrib.print_attributes o Toplevel.theory_of); +val print_methods = Toplevel.keep (Method.print_methods o Toplevel.theory_of); + + +(* print proof context contents *) + +val print_binds = Toplevel.keep (ProofContext.print_binds o Proof.context_of o Toplevel.proof_of); +val print_lthms = Toplevel.keep (ProofContext.print_thms o Proof.context_of o Toplevel.proof_of); + + +(* print theorems *) + +fun print_thms name = Toplevel.keep (fn state => + let + val prt_tthm = Attribute.pretty_tthm; + fun prt_tthms [th] = prt_tthm th + | prt_tthms ths = Pretty.block (Pretty.fbreaks (map prt_tthm ths)); + + val tthms = map (apfst (Thm.transfer (Toplevel.theory_of state))) + (Toplevel.node_cases PureThy.get_tthms (ProofContext.get_tthms o Proof.context_of) + state name); + in Pretty.writeln (prt_tthms tthms) end); + + +(* print types, terms and props *) + +fun read_typ thy = Sign.read_typ (Theory.sign_of thy, K None); + +fun read_term T thy s = + Thm.term_of (#1 (Thm.read_def_cterm (Theory.sign_of thy, K None, K None) [] true (s, T))); + + +fun print_type s = Toplevel.keep (fn state => + let + val sign = Toplevel.sign_of state; + val T = Toplevel.node_cases read_typ (ProofContext.read_typ o Proof.context_of) state s; + in Pretty.writeln (Pretty.quote (Sign.pretty_typ sign T)) end); + +fun print_term s = Toplevel.keep (fn state => + let + val sign = Toplevel.sign_of state; + val t = Toplevel.node_cases (read_term (TVar (("'z", 0), logicS))) + (ProofContext.read_term o Proof.context_of) state s; + val T = Term.type_of t; + in + Pretty.writeln (Pretty.block [Pretty.quote (Sign.pretty_term sign t), Pretty.fbrk, + Pretty.str "::", Pretty.brk 1, Pretty.quote (Sign.pretty_typ sign T)]) + end); + +fun print_prop s = Toplevel.keep (fn state => + let + val sign = Toplevel.sign_of state; + val prop = + Toplevel.node_cases (read_term propT) (ProofContext.read_prop o Proof.context_of) state s; + in Pretty.writeln (Pretty.quote (Sign.pretty_term sign prop)) end); + + +end;