Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified text folds: proof ... qed counts as extra block;
authorwenzelm
Wed, 08 Jul 2015 15:37:32 +0200
changeset 60694 b3fa4a8cdb5f
parent 60693 044f8bb3dd30
child 60695 757549b4bbe6
clarified text folds: proof ... qed counts as extra block;
src/Pure/Isar/keyword.ML file | annotate | diff | comparison | revisions
src/Pure/Isar/keyword.scala file | annotate | diff | comparison | revisions
src/Pure/Isar/outer_syntax.scala file | annotate | diff | comparison | revisions
src/Pure/Pure.thy file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/keyword.ML	Wed Jul 08 14:30:00 2015 +0200
+++ b/src/Pure/Isar/keyword.ML	Wed Jul 08 15:37:32 2015 +0200
@@ -22,6 +22,7 @@
   val qed_global: string
   val prf_goal: string
   val prf_block: string
+  val next_block: string
   val prf_open: string
   val prf_close: string
   val prf_chain: string
@@ -92,6 +93,7 @@
 val qed_global = "qed_global";
 val prf_goal = "prf_goal";
 val prf_block = "prf_block";
+val next_block = "next_block";
 val prf_open = "prf_open";
 val prf_close = "prf_close";
 val prf_chain = "prf_chain";
@@ -104,9 +106,9 @@
 
 val kinds =
   [diag, document_heading, document_body, document_raw, thy_begin, thy_end, thy_load, thy_decl,
-    thy_decl_block, thy_goal, qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open,
-    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal,
-    prf_script_asm_goal];
+    thy_decl_block, thy_goal, qed, qed_script, qed_block, qed_global, prf_goal, prf_block,
+    next_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script,
+    prf_script_goal, prf_script_asm_goal];
 
 
 (* specifications *)
@@ -243,13 +245,13 @@
   [thy_load, thy_decl, thy_decl_block, thy_goal];
 
 val is_proof = command_category
-  [qed, qed_script, qed_block, qed_global, prf_goal, prf_block, prf_open, prf_close,
-    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal,
+  [qed, qed_script, qed_block, qed_global, prf_goal, prf_block, next_block, prf_open,
+    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal,
     prf_script_asm_goal];
 
 val is_proof_body = command_category
-  [diag, document_heading, document_body, document_raw, prf_block, prf_open, prf_close,
-    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal,
+  [diag, document_heading, document_body, document_raw, prf_block, next_block, prf_open,
+    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal,
     prf_script_asm_goal];
 
 val is_theory_goal = command_category [thy_goal];
--- a/src/Pure/Isar/keyword.scala	Wed Jul 08 14:30:00 2015 +0200
+++ b/src/Pure/Isar/keyword.scala	Wed Jul 08 15:37:32 2015 +0200
@@ -29,6 +29,7 @@
   val QED_GLOBAL = "qed_global"
   val PRF_GOAL = "prf_goal"
   val PRF_BLOCK = "prf_block"
+  val NEXT_BLOCK = "next_block"
   val PRF_OPEN = "prf_open"
   val PRF_CLOSE = "prf_close"
   val PRF_CHAIN = "prf_chain"
@@ -63,13 +64,13 @@
   val theory_body = Set(THY_LOAD, THY_DECL, THY_DECL_BLOCK, THY_GOAL)
 
   val proof =
-    Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
-      PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL,
+    Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, NEXT_BLOCK, PRF_OPEN,
+      PRF_CLOSE, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL,
       PRF_SCRIPT_ASM_GOAL)
 
   val proof_body =
-    Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
-      PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL,
+    Set(DIAG, DOCUMENT_HEADING, DOCUMENT_BODY, DOCUMENT_RAW, PRF_BLOCK, NEXT_BLOCK, PRF_OPEN,
+      PRF_CLOSE, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT, PRF_SCRIPT_GOAL,
       PRF_SCRIPT_ASM_GOAL)
 
   val theory_goal = Set(THY_GOAL)
--- a/src/Pure/Isar/outer_syntax.scala	Wed Jul 08 14:30:00 2015 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Wed Jul 08 15:37:32 2015 +0200
@@ -166,6 +166,8 @@
           if (tok.is_command) {
             if (tok.is_command_kind(keywords, Keyword.theory_goal)) (2, 1)
             else if (tok.is_command_kind(keywords, Keyword.theory)) (1, 0)
+            else if (tok.is_command_kind(keywords, Keyword.PRF_BLOCK == _)) (y + 2, y + 1)
+            else if (tok.is_command_kind(keywords, Keyword.QED_BLOCK == _)) (y + 1, y - 3)
             else if (tok.is_command_kind(keywords, Keyword.proof_open)) (y + 2, y + 1)
             else if (tok.is_command_kind(keywords, Keyword.proof_close)) (y + 1, y - 1)
             else if (tok.is_command_kind(keywords, Keyword.qed_global)) (1, 0)
--- a/src/Pure/Pure.thy	Wed Jul 08 14:30:00 2015 +0200
+++ b/src/Pure/Pure.thy	Wed Jul 08 15:37:32 2015 +0200
@@ -62,7 +62,7 @@
   and "case" :: prf_asm % "proof"
   and "{" :: prf_open % "proof"
   and "}" :: prf_close % "proof"
-  and "next" :: prf_block % "proof"
+  and "next" :: next_block % "proof"
   and "qed" :: qed_block % "proof"
   and "by" ".." "." "sorry" :: "qed" % "proof"
   and "done" :: "qed_script" % "proof"
isabelle