src/Pure/Isar/outer_keyword.ML
changeset 36315 e859879079c8
parent 34243 8821e3293702
child 36681 dffeca08d3bf
     1.1 --- a/src/Pure/Isar/outer_keyword.ML	Fri Apr 23 19:36:23 2010 +0200
     1.2 +++ b/src/Pure/Isar/outer_keyword.ML	Fri Apr 23 21:00:28 2010 +0200
     1.3 @@ -17,6 +17,7 @@
     1.4    val thy_decl: T
     1.5    val thy_script: T
     1.6    val thy_goal: T
     1.7 +  val thy_schematic_goal: T
     1.8    val qed: T
     1.9    val qed_block: T
    1.10    val qed_global: T
    1.11 @@ -55,6 +56,7 @@
    1.12    val is_proof: string -> bool
    1.13    val is_theory_goal: string -> bool
    1.14    val is_proof_goal: string -> bool
    1.15 +  val is_schematic_goal: string -> bool
    1.16    val is_qed: string -> bool
    1.17    val is_qed_global: string -> bool
    1.18  end;
    1.19 @@ -81,6 +83,7 @@
    1.20  val thy_decl = kind "theory-decl";
    1.21  val thy_script = kind "theory-script";
    1.22  val thy_goal = kind "theory-goal";
    1.23 +val thy_schematic_goal = kind "theory-schematic-goal";
    1.24  val qed = kind "qed";
    1.25  val qed_block = kind "qed-block";
    1.26  val qed_global = kind "qed-global";
    1.27 @@ -95,9 +98,11 @@
    1.28  val prf_asm_goal = kind "proof-asm-goal";
    1.29  val prf_script = kind "proof-script";
    1.30  
    1.31 -val kinds = [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script,
    1.32 -  thy_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
    1.33 -  prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script] |> map kind_of;
    1.34 +val kinds =
    1.35 +  [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal,
    1.36 +    thy_schematic_goal, qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open,
    1.37 +    prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script]
    1.38 + |> map kind_of;
    1.39  
    1.40  
    1.41  (* tags *)
    1.42 @@ -191,14 +196,15 @@
    1.43  val is_theory_begin = command_category [thy_begin];
    1.44  
    1.45  val is_theory = command_category
    1.46 -  [thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal];
    1.47 +  [thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_script, thy_goal, thy_schematic_goal];
    1.48  
    1.49  val is_proof = command_category
    1.50    [qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close,
    1.51      prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
    1.52  
    1.53 -val is_theory_goal = command_category [thy_goal];
    1.54 +val is_theory_goal = command_category [thy_goal, thy_schematic_goal];
    1.55  val is_proof_goal = command_category [prf_goal, prf_asm_goal];
    1.56 +val is_schematic_goal = command_category [thy_schematic_goal];
    1.57  val is_qed = command_category [qed, qed_block];
    1.58  val is_qed_global = command_category [qed_global];
    1.59