--- a/lib/scripts/keywords Fri Mar 16 20:45:47 2012 +0100
+++ b/lib/scripts/keywords Fri Mar 16 21:20:23 2012 +0100
@@ -33,14 +33,19 @@
my %convert_kinds = (
"thy_begin" => "theory-begin",
"thy_end" => "theory-end",
- "thy_heading" => "theory-heading",
+ "thy_heading1" => "theory-heading",
+ "thy_heading2" => "theory-heading",
+ "thy_heading3" => "theory-heading",
+ "thy_heading4" => "theory-heading",
"thy_decl" => "theory-decl",
"thy_script" => "theory-script",
"thy_goal" => "theory-goal",
"thy_schematic_goal" => "theory-goal",
"qed_block" => "qed-block",
"qed_global" => "qed-global",
- "prf_heading" => "proof-heading",
+ "prf_heading2" => "proof-heading",
+ "prf_heading3" => "proof-heading",
+ "prf_heading4" => "proof-heading",
"prf_goal" => "proof-goal",
"prf_block" => "proof-block",
"prf_open" => "proof-open",
--- a/src/Pure/Isar/isar_syn.ML Fri Mar 16 20:45:47 2012 +0100
+++ b/src/Pure/Isar/isar_syn.ML Fri Mar 16 21:20:23 2012 +0100
@@ -47,22 +47,22 @@
val _ =
Outer_Syntax.markup_command Thy_Output.Markup
- ("chapter", Keyword.thy_heading) "chapter heading"
+ ("chapter", Keyword.thy_heading1) "chapter heading"
(Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
val _ =
Outer_Syntax.markup_command Thy_Output.Markup
- ("section", Keyword.thy_heading) "section heading"
+ ("section", Keyword.thy_heading2) "section heading"
(Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
val _ =
Outer_Syntax.markup_command Thy_Output.Markup
- ("subsection", Keyword.thy_heading) "subsection heading"
+ ("subsection", Keyword.thy_heading3) "subsection heading"
(Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
val _ =
Outer_Syntax.markup_command Thy_Output.Markup
- ("subsubsection", Keyword.thy_heading) "subsubsection heading"
+ ("subsubsection", Keyword.thy_heading4) "subsubsection heading"
(Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
val _ =
@@ -77,17 +77,17 @@
val _ =
Outer_Syntax.markup_command Thy_Output.Markup
- ("sect", Keyword.tag_proof Keyword.prf_heading) "formal comment (proof)"
+ ("sect", Keyword.tag_proof Keyword.prf_heading2) "formal comment (proof)"
(Parse.doc_source >> Isar_Cmd.proof_markup);
val _ =
Outer_Syntax.markup_command Thy_Output.Markup
- ("subsect", Keyword.tag_proof Keyword.prf_heading) "formal comment (proof)"
+ ("subsect", Keyword.tag_proof Keyword.prf_heading3) "formal comment (proof)"
(Parse.doc_source >> Isar_Cmd.proof_markup);
val _ =
Outer_Syntax.markup_command Thy_Output.Markup
- ("subsubsect", Keyword.tag_proof Keyword.prf_heading) "formal comment (proof)"
+ ("subsubsect", Keyword.tag_proof Keyword.prf_heading4) "formal comment (proof)"
(Parse.doc_source >> Isar_Cmd.proof_markup);
val _ =
--- a/src/Pure/Isar/keyword.ML Fri Mar 16 20:45:47 2012 +0100
+++ b/src/Pure/Isar/keyword.ML Fri Mar 16 21:20:23 2012 +0100
@@ -12,7 +12,10 @@
val diag: T
val thy_begin: T
val thy_end: T
- val thy_heading: T
+ val thy_heading1: T
+ val thy_heading2: T
+ val thy_heading3: T
+ val thy_heading4: T
val thy_decl: T
val thy_script: T
val thy_goal: T
@@ -20,7 +23,9 @@
val qed: T
val qed_block: T
val qed_global: T
- val prf_heading: T
+ val prf_heading2: T
+ val prf_heading3: T
+ val prf_heading4: T
val prf_goal: T
val prf_block: T
val prf_open: T
@@ -78,7 +83,10 @@
val diag = kind "diag";
val thy_begin = kind "thy_begin";
val thy_end = kind "thy_end";
-val thy_heading = kind "thy_heading";
+val thy_heading1 = kind "thy_heading1";
+val thy_heading2 = kind "thy_heading2";
+val thy_heading3 = kind "thy_heading3";
+val thy_heading4 = kind "thy_heading4";
val thy_decl = kind "thy_decl";
val thy_script = kind "thy_script";
val thy_goal = kind "thy_goal";
@@ -86,7 +94,9 @@
val qed = kind "qed";
val qed_block = kind "qed_block";
val qed_global = kind "qed_global";
-val prf_heading = kind "prf_heading";
+val prf_heading2 = kind "prf_heading2";
+val prf_heading3 = kind "prf_heading3";
+val prf_heading4 = kind "prf_heading4";
val prf_goal = kind "prf_goal";
val prf_block = kind "prf_block";
val prf_open = kind "prf_open";
@@ -98,8 +108,9 @@
val prf_script = kind "prf_script";
val kinds =
- [control, diag, thy_begin, thy_end, thy_heading, thy_decl, thy_script, thy_goal,
- thy_schematic_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open,
+ [control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
+ thy_decl, thy_script, thy_goal, thy_schematic_goal, qed, qed_block, qed_global,
+ prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open,
prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
@@ -222,16 +233,20 @@
val is_control = command_category [control];
val is_regular = not o command_category [diag, control];
-val is_heading = command_category [thy_heading, prf_heading];
+val is_heading =
+ command_category [thy_heading1, thy_heading2, thy_heading3, thy_heading4,
+ prf_heading2, prf_heading3, prf_heading4];
val is_theory_begin = command_category [thy_begin];
val is_theory = command_category
- [thy_begin, thy_end, thy_heading, thy_decl, thy_script, thy_goal, thy_schematic_goal];
+ [thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
+ thy_decl, thy_script, thy_goal, thy_schematic_goal];
val is_proof = command_category
- [qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
- prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
+ [qed, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
+ prf_goal, prf_block, prf_open, prf_close, prf_chain, prf_decl,
+ prf_asm, prf_asm_goal, prf_script];
val is_theory_goal = command_category [thy_goal, thy_schematic_goal];
val is_proof_goal = command_category [prf_goal, prf_asm_goal];
--- a/src/Pure/Isar/keyword.scala Fri Mar 16 20:45:47 2012 +0100
+++ b/src/Pure/Isar/keyword.scala Fri Mar 16 21:20:23 2012 +0100
@@ -16,7 +16,10 @@
val DIAG = "diag"
val THY_BEGIN = "thy_begin"
val THY_END = "thy_end"
- val THY_HEADING = "thy_heading"
+ val THY_HEADING1 = "thy_heading1"
+ val THY_HEADING2 = "thy_heading2"
+ val THY_HEADING3 = "thy_heading3"
+ val THY_HEADING4 = "thy_heading4"
val THY_DECL = "thy_decl"
val THY_SCRIPT = "thy_script"
val THY_GOAL = "thy_goal"
@@ -24,7 +27,9 @@
val QED = "qed"
val QED_BLOCK = "qed_block"
val QED_GLOBAL = "qed_global"
- val PRF_HEADING = "prf_heading"
+ val PRF_HEADING2 = "prf_heading2"
+ val PRF_HEADING3 = "prf_heading3"
+ val PRF_HEADING4 = "prf_heading4"
val PRF_GOAL = "prf_goal"
val PRF_BLOCK = "prf_block"
val PRF_OPEN = "prf_open"
@@ -42,12 +47,13 @@
val control = Set(CONTROL)
val diag = Set(DIAG)
val theory =
- Set(THY_BEGIN, THY_END, THY_HEADING, THY_DECL, THY_SCRIPT, THY_GOAL, THY_SCHEMATIC_GOAL)
+ Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
+ THY_DECL, THY_SCRIPT, THY_GOAL, THY_SCHEMATIC_GOAL)
val theory1 = Set(THY_BEGIN, THY_END)
val theory2 = Set(THY_DECL, THY_GOAL)
val proof =
- Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING, PRF_GOAL, PRF_BLOCK,
- PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT)
+ Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, PRF_GOAL,
+ PRF_BLOCK, PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT)
val proof1 =
Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)
--- a/src/Pure/Isar/outer_syntax.scala Fri Mar 16 20:45:47 2012 +0100
+++ b/src/Pure/Isar/outer_syntax.scala Fri Mar 16 21:20:23 2012 +0100
@@ -68,19 +68,17 @@
}
def heading_level(name: String): Option[Int] =
- name match {
- // FIXME avoid hard-wired info!?
- case "header" => Some(1)
- case "chapter" => Some(2)
- case "section" | "sect" => Some(3)
- case "subsection" | "subsect" => Some(4)
- case "subsubsection" | "subsubsect" => Some(5)
- case _ =>
- keyword_kind(name) match {
- case Some(kind) if Keyword.theory(kind) => Some(6)
- case _ => None
- }
+ {
+ keyword_kind(name) match {
+ case _ if name == "header" => Some(0)
+ case Some(Keyword.THY_HEADING1) => Some(1)
+ case Some(Keyword.THY_HEADING2) | Some(Keyword.PRF_HEADING2) => Some(2)
+ case Some(Keyword.THY_HEADING3) | Some(Keyword.PRF_HEADING3) => Some(3)
+ case Some(Keyword.THY_HEADING4) | Some(Keyword.PRF_HEADING4) => Some(4)
+ case Some(kind) if Keyword.theory(kind) => Some(5)
+ case _ => None
}
+ }
def heading_level(command: Command): Option[Int] =
heading_level(command.name)
--- a/src/Pure/ProofGeneral/pgip_parser.ML Fri Mar 16 20:45:47 2012 +0100
+++ b/src/Pure/ProofGeneral/pgip_parser.ML Fri Mar 16 21:20:23 2012 +0100
@@ -57,7 +57,10 @@
|> command Keyword.diag (fn text => [D.Spuriouscmd {text = text}])
|> command Keyword.thy_begin thy_begin
|> command Keyword.thy_end (fn text => [D.Closeblock {}, D.Closetheory {text = text}])
- |> command Keyword.thy_heading thy_heading
+ |> command Keyword.thy_heading1 thy_heading
+ |> command Keyword.thy_heading2 thy_heading
+ |> command Keyword.thy_heading3 thy_heading
+ |> command Keyword.thy_heading4 thy_heading
|> command Keyword.thy_decl thy_decl
|> command Keyword.thy_script thy_decl
|> command Keyword.thy_goal goal
@@ -65,7 +68,9 @@
|> command Keyword.qed closegoal
|> command Keyword.qed_block closegoal
|> command Keyword.qed_global (fn text => [D.Giveupgoal {text = text}])
- |> command Keyword.prf_heading (fn text => [D.Doccomment {text = text}])
+ |> command Keyword.prf_heading2 (fn text => [D.Doccomment {text = text}])
+ |> command Keyword.prf_heading3 (fn text => [D.Doccomment {text = text}])
+ |> command Keyword.prf_heading4 (fn text => [D.Doccomment {text = text}])
|> command Keyword.prf_goal goal
|> command Keyword.prf_block prf_block
|> command Keyword.prf_open prf_open
--- a/src/Pure/Thy/thy_syntax.scala Fri Mar 16 20:45:47 2012 +0100
+++ b/src/Pure/Thy/thy_syntax.scala Fri Mar 16 21:20:23 2012 +0100
@@ -57,8 +57,8 @@
{
syntax.heading_level(command) match {
case Some(i) =>
- close(_ >= i)
- stack = (i, command.source, buffer()) :: stack
+ close(_ > i)
+ stack = (i + 1, command.source, buffer()) :: stack
case None =>
}
stack.head._3 += Atom(command)