# HG changeset patch
# User wenzelm
# Date 1291494415 -3600
# Node ID 9e54eb514a4618b49f13114615a1f570b24e377f
# Parent  49765c1104d4267610e6532f276230ad30f6eb9c
formal notepad without any result;

diff -r 49765c1104d4 -r 9e54eb514a46 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Sat Dec 04 18:41:12 2010 +0100
+++ b/etc/isar-keywords-ZF.el	Sat Dec 04 21:26:55 2010 +0100
@@ -107,6 +107,7 @@
     "nonterminals"
     "notation"
     "note"
+    "notepad"
     "obtain"
     "oops"
     "oracle"
@@ -383,6 +384,7 @@
     "no_type_notation"
     "nonterminals"
     "notation"
+    "notepad"
     "oracle"
     "overloading"
     "parse_ast_translation"
diff -r 49765c1104d4 -r 9e54eb514a46 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Sat Dec 04 18:41:12 2010 +0100
+++ b/etc/isar-keywords.el	Sat Dec 04 21:26:55 2010 +0100
@@ -144,6 +144,7 @@
     "nonterminals"
     "notation"
     "note"
+    "notepad"
     "obtain"
     "oops"
     "oracle"
@@ -489,6 +490,7 @@
     "nominal_datatype"
     "nonterminals"
     "notation"
+    "notepad"
     "oracle"
     "overloading"
     "parse_ast_translation"
diff -r 49765c1104d4 -r 9e54eb514a46 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Sat Dec 04 18:41:12 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Sat Dec 04 21:26:55 2010 +0100
@@ -35,7 +35,8 @@
 
 val _ =
   Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
-    (Scan.succeed (Toplevel.exit o Toplevel.end_local_theory));
+    (Scan.succeed
+      (Toplevel.exit o Toplevel.end_local_theory o Toplevel.end_proof (K Proof.end_notepad)));
 
 
 
@@ -507,6 +508,11 @@
 val _ = gen_theorem true Thm.corollaryK;
 
 val _ =
+  Outer_Syntax.local_theory_to_proof "notepad"
+    "Isar proof state as formal notepad, without any result" Keyword.thy_decl
+    (Parse.begin >> K Proof.begin_notepad);
+
+val _ =
   Outer_Syntax.local_theory_to_proof "example_proof"
     "example proof body, without any result" Keyword.thy_schematic_goal
     (Scan.succeed
diff -r 49765c1104d4 -r 9e54eb514a46 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Dec 04 18:41:12 2010 +0100
+++ b/src/Pure/Isar/proof.ML	Sat Dec 04 21:26:55 2010 +0100
@@ -76,6 +76,8 @@
   val begin_block: state -> state
   val next_block: state -> state
   val end_block: state -> state
+  val begin_notepad: Proof.context -> state
+  val end_notepad: state -> Proof.context
   val proof: Method.text option -> state -> state Seq.seq
   val defer: int option -> state -> state Seq.seq
   val prefer: int -> state -> state Seq.seq
@@ -767,12 +769,30 @@
 fun end_block state =
   state
   |> assert_forward
+  |> assert_bottom false
   |> close_block
   |> assert_current_goal false
   |> close_block
   |> export_facts state;
 
 
+(* global notepad *)
+
+val begin_notepad =
+  init
+  #> open_block
+  #> map_context (Variable.set_body true)
+  #> open_block;
+
+val end_notepad =
+  assert_forward
+  #> assert_bottom true
+  #> close_block
+  #> assert_current_goal false
+  #> close_block
+  #> context_of;
+
+
 (* sub-proofs *)
 
 fun proof opt_text =
diff -r 49765c1104d4 -r 9e54eb514a46 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sat Dec 04 18:41:12 2010 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sat Dec 04 21:26:55 2010 +0100
@@ -486,12 +486,13 @@
     let
       val prf = init int gthy;
       val skip = ! skip_proofs;
-      val schematic = Proof.schematic_goal prf;
+      val (is_goal, no_skip) =
+        (true, Proof.schematic_goal prf) handle ERROR _ => (false, true);
     in
-      if skip andalso schematic then
+      if is_goal andalso skip andalso no_skip then
         warning "Cannot skip proof of schematic goal statement"
       else ();
-      if skip andalso not schematic then
+      if skip andalso not no_skip then
         SkipProof (0, (finish gthy (Proof.global_skip_proof int prf), gthy))
       else Proof (Proof_Node.init prf, (finish gthy, gthy))
     end