print_context;
authorwenzelm
Fri Aug 20 15:44:29 1999 +0200 (1999-08-20 ago)
changeset 7308e01aab03a2a1
parent 7307 c065073cdb34
child 7309 838a7bc92d81
print_context;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/toplevel.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Aug 20 15:43:25 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri Aug 20 15:44:29 1999 +0200
     1.3 @@ -32,6 +32,7 @@
     1.4    val update_thy: string -> Toplevel.transition -> Toplevel.transition
     1.5    val update_thy_only: string -> Toplevel.transition -> Toplevel.transition
     1.6    val pretty_setmargin: int -> Toplevel.transition -> Toplevel.transition
     1.7 +  val print_context: Toplevel.transition -> Toplevel.transition
     1.8    val print_theory: Toplevel.transition -> Toplevel.transition
     1.9    val print_syntax: Toplevel.transition -> Toplevel.transition
    1.10    val print_theorems: Toplevel.transition -> Toplevel.transition
    1.11 @@ -127,8 +128,9 @@
    1.12  fun pretty_setmargin n = Toplevel.imperative (fn () => Pretty.setmargin n);
    1.13  
    1.14  
    1.15 -(* print theory contents *)
    1.16 +(* print theory *)
    1.17  
    1.18 +val print_context = Toplevel.keep Toplevel.print_state_context;
    1.19  val print_theory = Toplevel.keep (PureThy.print_theory o Toplevel.theory_of);
    1.20  val print_syntax = Toplevel.keep (Display.print_syntax o Toplevel.theory_of);
    1.21  val print_theorems = Toplevel.keep (PureThy.print_theorems o Toplevel.theory_of);
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Aug 20 15:43:25 1999 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Aug 20 15:44:29 1999 +0200
     2.3 @@ -440,6 +440,10 @@
     2.4    OuterSyntax.improper_command "help" "print outer syntax (global)" K.diag
     2.5      (Scan.succeed (Toplevel.imperative OuterSyntax.print_outer_syntax));
     2.6  
     2.7 +val print_contextP =
     2.8 +  OuterSyntax.improper_command "print_context" "print theory context name" K.diag
     2.9 +    (Scan.succeed IsarCmd.print_context);
    2.10 +
    2.11  val print_theoryP =
    2.12    OuterSyntax.improper_command "print_theory" "print logical theory contents (verbose!)" K.diag
    2.13      (Scan.succeed IsarCmd.print_theory);
    2.14 @@ -587,9 +591,10 @@
    2.15    skip_proofP, applyP, then_applyP, proofP, alsoP, finallyP, backP,
    2.16    cannot_undoP, clear_undoP, redoP, undos_proofP, kill_proofP, undoP,
    2.17    (*diagnostic commands*)
    2.18 -  pretty_setmarginP, print_commandsP, print_theoryP, print_syntaxP,
    2.19 -  print_attributesP, print_methodsP, print_theoremsP, print_bindsP,
    2.20 -  print_lthmsP, print_thmsP, print_propP, print_termP, print_typeP,
    2.21 +  pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
    2.22 +  print_syntaxP, print_attributesP, print_methodsP, print_theoremsP,
    2.23 +  print_bindsP, print_lthmsP, print_thmsP, print_propP, print_termP,
    2.24 +  print_typeP,
    2.25    (*system commands*)
    2.26    cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
    2.27    touch_thyP, touch_all_thysP, remove_thyP, prP, disable_prP,
     3.1 --- a/src/Pure/Isar/toplevel.ML	Fri Aug 20 15:43:25 1999 +0200
     3.2 +++ b/src/Pure/Isar/toplevel.ML	Fri Aug 20 15:44:29 1999 +0200
     3.3 @@ -12,6 +12,7 @@
     3.4    val toplevel: state
     3.5    val prompt_state_default: state -> string
     3.6    val prompt_state_fn: (state -> string) ref
     3.7 +  val print_state_context: state -> unit
     3.8    val print_state_default: state -> unit
     3.9    val print_state_fn: (state -> unit) ref
    3.10    val print_state: state -> unit
    3.11 @@ -74,10 +75,16 @@
    3.12  fun str_of_node (Theory _) = "in theory mode"
    3.13    | str_of_node (Proof _) = "in proof mode";
    3.14  
    3.15 -fun print_node (Theory thy) = Pretty.writeln (Pretty.block
    3.16 -      [Pretty.str "Theory:", Pretty.brk 1, Pretty.str (PureThy.get_name thy),
    3.17 -        Pretty.str " =", Pretty.brk 1, Display.pretty_theory thy])
    3.18 -  | print_node (Proof prf) = Proof.print_state (ProofHistory.position prf) (ProofHistory.current prf);
    3.19 +fun print_ctxt thy = Pretty.writeln (Pretty.block
    3.20 +  [Pretty.str "Theory:", Pretty.brk 1, Pretty.str (PureThy.get_name thy),
    3.21 +    Pretty.str " =", Pretty.brk 1, Display.pretty_theory thy]);
    3.22 +
    3.23 +fun print_node_ctxt (Theory thy) = print_ctxt thy
    3.24 +  | print_node_ctxt (Proof prf) = print_ctxt (Proof.theory_of (ProofHistory.current prf));
    3.25 +
    3.26 +fun print_node (Theory thy) = print_ctxt thy
    3.27 +  | print_node (Proof prf) = Proof.print_state (ProofHistory.position prf)
    3.28 +      (ProofHistory.current prf);
    3.29  
    3.30  
    3.31  (* datatype state *)
    3.32 @@ -100,15 +107,17 @@
    3.33  fun prompt_state state = ! prompt_state_fn state;
    3.34  
    3.35  
    3.36 -(* print_state hook *)
    3.37 +(* print state *)
    3.38  
    3.39 -fun print_topnode (State []) = ()
    3.40 -  | print_topnode (State ((node, _) :: _)) = print_node (History.current node);
    3.41 +fun print_topnode _ (State []) = ()
    3.42 +  | print_topnode prt (State ((node, _) :: _)) = prt (History.current node);
    3.43 +
    3.44 +val print_state_context = print_topnode print_node_ctxt;
    3.45  
    3.46  fun print_state_default state =
    3.47    let val ref (begin_state, end_state, _) = Goals.current_goals_markers in
    3.48      if begin_state = "" then () else writeln begin_state;
    3.49 -    print_topnode state;
    3.50 +    print_topnode print_node state;
    3.51      if end_state = "" then () else writeln end_state
    3.52    end;
    3.53