# HG changeset patch # User wenzelm # Date 1331929223 -3600 # Node ID 481b7d9ad6fee22551db76e3a3b6c7834bc9cbd9 # Parent 38aaa08fb37f52acfb2dd69251ebcf29ad186428 more abstract heading level; diff -r 38aaa08fb37f -r 481b7d9ad6fe lib/scripts/keywords --- 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", diff -r 38aaa08fb37f -r 481b7d9ad6fe src/Pure/Isar/isar_syn.ML --- 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 _ = diff -r 38aaa08fb37f -r 481b7d9ad6fe src/Pure/Isar/keyword.ML --- 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]; diff -r 38aaa08fb37f -r 481b7d9ad6fe src/Pure/Isar/keyword.scala --- 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) diff -r 38aaa08fb37f -r 481b7d9ad6fe src/Pure/Isar/outer_syntax.scala --- 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) diff -r 38aaa08fb37f -r 481b7d9ad6fe src/Pure/ProofGeneral/pgip_parser.ML --- 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 diff -r 38aaa08fb37f -r 481b7d9ad6fe src/Pure/Thy/thy_syntax.scala --- 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)