1.1 --- a/lib/scripts/keywords	Fri Mar 16 20:45:47 2012 +0100
     1.2 +++ b/lib/scripts/keywords	Fri Mar 16 21:20:23 2012 +0100
     1.3 @@ -33,14 +33,19 @@
     1.4  my %convert_kinds = (
     1.5    "thy_begin" => "theory-begin",
     1.6    "thy_end" => "theory-end",
     1.7 -  "thy_heading" => "theory-heading",
     1.8 +  "thy_heading1" => "theory-heading",
     1.9 +  "thy_heading2" => "theory-heading",
    1.10 +  "thy_heading3" => "theory-heading",
    1.11 +  "thy_heading4" => "theory-heading",
    1.12    "thy_decl" => "theory-decl",
    1.13    "thy_script" => "theory-script",
    1.14    "thy_goal" => "theory-goal",
    1.15    "thy_schematic_goal" => "theory-goal",
    1.16    "qed_block" => "qed-block",
    1.17    "qed_global" => "qed-global",
    1.18 -  "prf_heading" => "proof-heading",
    1.19 +  "prf_heading2" => "proof-heading",
    1.20 +  "prf_heading3" => "proof-heading",
    1.21 +  "prf_heading4" => "proof-heading",
    1.22    "prf_goal" => "proof-goal",
    1.23    "prf_block" => "proof-block",
    1.24    "prf_open" => "proof-open",

     2.1 --- a/src/Pure/Isar/isar_syn.ML	Fri Mar 16 20:45:47 2012 +0100
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Fri Mar 16 21:20:23 2012 +0100
     2.3 @@ -47,22 +47,22 @@
     2.4  
     2.5  val _ =
     2.6    Outer_Syntax.markup_command Thy_Output.Markup
     2.7 -    ("chapter", Keyword.thy_heading) "chapter heading"
     2.8 +    ("chapter", Keyword.thy_heading1) "chapter heading"
     2.9      (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
    2.10  
    2.11  val _ =
    2.12    Outer_Syntax.markup_command Thy_Output.Markup
    2.13 -    ("section", Keyword.thy_heading) "section heading"
    2.14 +    ("section", Keyword.thy_heading2) "section heading"
    2.15      (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
    2.16  
    2.17  val _ =
    2.18    Outer_Syntax.markup_command Thy_Output.Markup
    2.19 -    ("subsection", Keyword.thy_heading) "subsection heading"
    2.20 +    ("subsection", Keyword.thy_heading3) "subsection heading"
    2.21      (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
    2.22  
    2.23  val _ =
    2.24    Outer_Syntax.markup_command Thy_Output.Markup
    2.25 -    ("subsubsection", Keyword.thy_heading) "subsubsection heading"
    2.26 +    ("subsubsection", Keyword.thy_heading4) "subsubsection heading"
    2.27      (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
    2.28  
    2.29  val _ =
    2.30 @@ -77,17 +77,17 @@
    2.31  
    2.32  val _ =
    2.33    Outer_Syntax.markup_command Thy_Output.Markup
    2.34 -    ("sect", Keyword.tag_proof Keyword.prf_heading) "formal comment (proof)"
    2.35 +    ("sect", Keyword.tag_proof Keyword.prf_heading2) "formal comment (proof)"
    2.36      (Parse.doc_source >> Isar_Cmd.proof_markup);
    2.37  
    2.38  val _ =
    2.39    Outer_Syntax.markup_command Thy_Output.Markup
    2.40 -    ("subsect", Keyword.tag_proof Keyword.prf_heading) "formal comment (proof)"
    2.41 +    ("subsect", Keyword.tag_proof Keyword.prf_heading3) "formal comment (proof)"
    2.42      (Parse.doc_source >> Isar_Cmd.proof_markup);
    2.43  
    2.44  val _ =
    2.45    Outer_Syntax.markup_command Thy_Output.Markup
    2.46 -    ("subsubsect", Keyword.tag_proof Keyword.prf_heading) "formal comment (proof)"
    2.47 +    ("subsubsect", Keyword.tag_proof Keyword.prf_heading4) "formal comment (proof)"
    2.48      (Parse.doc_source >> Isar_Cmd.proof_markup);
    2.49  
    2.50  val _ =

     3.1 --- a/src/Pure/Isar/keyword.ML	Fri Mar 16 20:45:47 2012 +0100
     3.2 +++ b/src/Pure/Isar/keyword.ML	Fri Mar 16 21:20:23 2012 +0100
     3.3 @@ -12,7 +12,10 @@
     3.4    val diag: T
     3.5    val thy_begin: T
     3.6    val thy_end: T
     3.7 -  val thy_heading: T
     3.8 +  val thy_heading1: T
     3.9 +  val thy_heading2: T
    3.10 +  val thy_heading3: T
    3.11 +  val thy_heading4: T
    3.12    val thy_decl: T
    3.13    val thy_script: T
    3.14    val thy_goal: T
    3.15 @@ -20,7 +23,9 @@
    3.16    val qed: T
    3.17    val qed_block: T
    3.18    val qed_global: T
    3.19 -  val prf_heading: T
    3.20 +  val prf_heading2: T
    3.21 +  val prf_heading3: T
    3.22 +  val prf_heading4: T
    3.23    val prf_goal: T
    3.24    val prf_block: T
    3.25    val prf_open: T
    3.26 @@ -78,7 +83,10 @@
    3.27  val diag = kind "diag";
    3.28  val thy_begin = kind "thy_begin";
    3.29  val thy_end = kind "thy_end";
    3.30 -val thy_heading = kind "thy_heading";
    3.31 +val thy_heading1 = kind "thy_heading1";
    3.32 +val thy_heading2 = kind "thy_heading2";
    3.33 +val thy_heading3 = kind "thy_heading3";
    3.34 +val thy_heading4 = kind "thy_heading4";
    3.35  val thy_decl = kind "thy_decl";
    3.36  val thy_script = kind "thy_script";
    3.37  val thy_goal = kind "thy_goal";
    3.38 @@ -86,7 +94,9 @@
    3.39  val qed = kind "qed";
    3.40  val qed_block = kind "qed_block";
    3.41  val qed_global = kind "qed_global";
    3.42 -val prf_heading = kind "prf_heading";
    3.43 +val prf_heading2 = kind "prf_heading2";
    3.44 +val prf_heading3 = kind "prf_heading3";
    3.45 +val prf_heading4 = kind "prf_heading4";
    3.46  val prf_goal = kind "prf_goal";
    3.47  val prf_block = kind "prf_block";
    3.48  val prf_open = kind "prf_open";
    3.49 @@ -98,8 +108,9 @@
    3.50  val prf_script = kind "prf_script";
    3.51  
    3.52  val kinds =
    3.53 -  [control, diag, thy_begin, thy_end, thy_heading, thy_decl, thy_script, thy_goal,
    3.54 -    thy_schematic_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open,
    3.55 +  [control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
    3.56 +    thy_decl, thy_script, thy_goal, thy_schematic_goal, qed, qed_block, qed_global,
    3.57 +    prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open,
    3.58      prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
    3.59  
    3.60  
    3.61 @@ -222,16 +233,20 @@
    3.62  val is_control = command_category [control];
    3.63  val is_regular = not o command_category [diag, control];
    3.64  
    3.65 -val is_heading = command_category [thy_heading, prf_heading];
    3.66 +val is_heading =
    3.67 +  command_category [thy_heading1, thy_heading2, thy_heading3, thy_heading4,
    3.68 +    prf_heading2, prf_heading3, prf_heading4];
    3.69  
    3.70  val is_theory_begin = command_category [thy_begin];
    3.71  
    3.72  val is_theory = command_category
    3.73 -  [thy_begin, thy_end, thy_heading, thy_decl, thy_script, thy_goal, thy_schematic_goal];
    3.74 +  [thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
    3.75 +    thy_decl, thy_script, thy_goal, thy_schematic_goal];
    3.76  
    3.77  val is_proof = command_category
    3.78 -  [qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
    3.79 -    prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
    3.80 +  [qed, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
    3.81 +    prf_goal, prf_block, prf_open, prf_close, prf_chain, prf_decl,
    3.82 +    prf_asm, prf_asm_goal, prf_script];
    3.83  
    3.84  val is_theory_goal = command_category [thy_goal, thy_schematic_goal];
    3.85  val is_proof_goal = command_category [prf_goal, prf_asm_goal];

     4.1 --- a/src/Pure/Isar/keyword.scala	Fri Mar 16 20:45:47 2012 +0100
     4.2 +++ b/src/Pure/Isar/keyword.scala	Fri Mar 16 21:20:23 2012 +0100
     4.3 @@ -16,7 +16,10 @@
     4.4    val DIAG = "diag"
     4.5    val THY_BEGIN = "thy_begin"
     4.6    val THY_END = "thy_end"
     4.7 -  val THY_HEADING = "thy_heading"
     4.8 +  val THY_HEADING1 = "thy_heading1"
     4.9 +  val THY_HEADING2 = "thy_heading2"
    4.10 +  val THY_HEADING3 = "thy_heading3"
    4.11 +  val THY_HEADING4 = "thy_heading4"
    4.12    val THY_DECL = "thy_decl"
    4.13    val THY_SCRIPT = "thy_script"
    4.14    val THY_GOAL = "thy_goal"
    4.15 @@ -24,7 +27,9 @@
    4.16    val QED = "qed"
    4.17    val QED_BLOCK = "qed_block"
    4.18    val QED_GLOBAL = "qed_global"
    4.19 -  val PRF_HEADING = "prf_heading"
    4.20 +  val PRF_HEADING2 = "prf_heading2"
    4.21 +  val PRF_HEADING3 = "prf_heading3"
    4.22 +  val PRF_HEADING4 = "prf_heading4"
    4.23    val PRF_GOAL = "prf_goal"
    4.24    val PRF_BLOCK = "prf_block"
    4.25    val PRF_OPEN = "prf_open"
    4.26 @@ -42,12 +47,13 @@
    4.27    val control = Set(CONTROL)
    4.28    val diag = Set(DIAG)
    4.29    val theory =
    4.30 -    Set(THY_BEGIN, THY_END, THY_HEADING, THY_DECL, THY_SCRIPT, THY_GOAL, THY_SCHEMATIC_GOAL)
    4.31 +    Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
    4.32 +      THY_DECL, THY_SCRIPT, THY_GOAL, THY_SCHEMATIC_GOAL)
    4.33    val theory1 = Set(THY_BEGIN, THY_END)
    4.34    val theory2 = Set(THY_DECL, THY_GOAL)
    4.35    val proof =
    4.36 -    Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING, PRF_GOAL, PRF_BLOCK,
    4.37 -      PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT)
    4.38 +    Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, PRF_GOAL,
    4.39 +      PRF_BLOCK, PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT)
    4.40    val proof1 =
    4.41      Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
    4.42    val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)

     5.1 --- a/src/Pure/Isar/outer_syntax.scala	Fri Mar 16 20:45:47 2012 +0100
     5.2 +++ b/src/Pure/Isar/outer_syntax.scala	Fri Mar 16 21:20:23 2012 +0100
     5.3 @@ -68,19 +68,17 @@
     5.4      }
     5.5  
     5.6    def heading_level(name: String): Option[Int] =
     5.7 -    name match {
     5.8 -      // FIXME avoid hard-wired info!?
     5.9 -      case "header" => Some(1)
    5.10 -      case "chapter" => Some(2)
    5.11 -      case "section" | "sect" => Some(3)
    5.12 -      case "subsection" | "subsect" => Some(4)
    5.13 -      case "subsubsection" | "subsubsect" => Some(5)
    5.14 -      case _ =>
    5.15 -        keyword_kind(name) match {
    5.16 -          case Some(kind) if Keyword.theory(kind) => Some(6)
    5.17 -          case _ => None
    5.18 -        }
    5.19 +  {
    5.20 +    keyword_kind(name) match {
    5.21 +      case _ if name == "header" => Some(0)
    5.22 +      case Some(Keyword.THY_HEADING1) => Some(1)
    5.23 +      case Some(Keyword.THY_HEADING2) | Some(Keyword.PRF_HEADING2) => Some(2)
    5.24 +      case Some(Keyword.THY_HEADING3) | Some(Keyword.PRF_HEADING3) => Some(3)
    5.25 +      case Some(Keyword.THY_HEADING4) | Some(Keyword.PRF_HEADING4) => Some(4)
    5.26 +      case Some(kind) if Keyword.theory(kind) => Some(5)
    5.27 +      case _ => None
    5.28      }
    5.29 +  }
    5.30  
    5.31    def heading_level(command: Command): Option[Int] =
    5.32      heading_level(command.name)

     6.1 --- a/src/Pure/ProofGeneral/pgip_parser.ML	Fri Mar 16 20:45:47 2012 +0100
     6.2 +++ b/src/Pure/ProofGeneral/pgip_parser.ML	Fri Mar 16 21:20:23 2012 +0100
     6.3 @@ -57,7 +57,10 @@
     6.4    |> command Keyword.diag             (fn text => [D.Spuriouscmd {text = text}])
     6.5    |> command Keyword.thy_begin        thy_begin
     6.6    |> command Keyword.thy_end          (fn text => [D.Closeblock {}, D.Closetheory {text = text}])
     6.7 -  |> command Keyword.thy_heading      thy_heading
     6.8 +  |> command Keyword.thy_heading1     thy_heading
     6.9 +  |> command Keyword.thy_heading2     thy_heading
    6.10 +  |> command Keyword.thy_heading3     thy_heading
    6.11 +  |> command Keyword.thy_heading4     thy_heading
    6.12    |> command Keyword.thy_decl         thy_decl
    6.13    |> command Keyword.thy_script       thy_decl
    6.14    |> command Keyword.thy_goal         goal
    6.15 @@ -65,7 +68,9 @@
    6.16    |> command Keyword.qed              closegoal
    6.17    |> command Keyword.qed_block        closegoal
    6.18    |> command Keyword.qed_global       (fn text => [D.Giveupgoal {text = text}])
    6.19 -  |> command Keyword.prf_heading      (fn text => [D.Doccomment {text = text}])
    6.20 +  |> command Keyword.prf_heading2     (fn text => [D.Doccomment {text = text}])
    6.21 +  |> command Keyword.prf_heading3     (fn text => [D.Doccomment {text = text}])
    6.22 +  |> command Keyword.prf_heading4     (fn text => [D.Doccomment {text = text}])
    6.23    |> command Keyword.prf_goal         goal
    6.24    |> command Keyword.prf_block        prf_block
    6.25    |> command Keyword.prf_open         prf_open

     7.1 --- a/src/Pure/Thy/thy_syntax.scala	Fri Mar 16 20:45:47 2012 +0100
     7.2 +++ b/src/Pure/Thy/thy_syntax.scala	Fri Mar 16 21:20:23 2012 +0100
     7.3 @@ -57,8 +57,8 @@
     7.4        {
     7.5          syntax.heading_level(command) match {
     7.6            case Some(i) =>
     7.7 -            close(_ >= i)
     7.8 -            stack = (i, command.source, buffer()) :: stack
     7.9 +            close(_ > i)
    7.10 +            stack = (i + 1, command.source, buffer()) :: stack
    7.11            case None =>
    7.12          }
    7.13          stack.head._3 += Atom(command)