src/Pure/Isar/keyword.ML
changeset 69913 ca515cf61651
parent 67139 8fe0aba577af
     1.1 --- a/src/Pure/Isar/keyword.ML	Thu Mar 14 16:35:58 2019 +0100
     1.2 +++ b/src/Pure/Isar/keyword.ML	Thu Mar 14 16:55:06 2019 +0100
     1.3 @@ -14,8 +14,12 @@
     1.4    val thy_end: string
     1.5    val thy_decl: string
     1.6    val thy_decl_block: string
     1.7 +  val thy_defn: string
     1.8 +  val thy_stmt: string
     1.9    val thy_load: string
    1.10    val thy_goal: string
    1.11 +  val thy_goal_defn: string
    1.12 +  val thy_goal_stmt: string
    1.13    val qed: string
    1.14    val qed_script: string
    1.15    val qed_block: string
    1.16 @@ -93,8 +97,12 @@
    1.17  val thy_end = "thy_end";
    1.18  val thy_decl = "thy_decl";
    1.19  val thy_decl_block = "thy_decl_block";
    1.20 +val thy_defn = "thy_defn";
    1.21 +val thy_stmt = "thy_stmt";
    1.22  val thy_load = "thy_load";
    1.23  val thy_goal = "thy_goal";
    1.24 +val thy_goal_defn = "thy_goal_defn";
    1.25 +val thy_goal_stmt = "thy_goal_stmt";
    1.26  val qed = "qed";
    1.27  val qed_script = "qed_script";
    1.28  val qed_block = "qed_block";
    1.29 @@ -117,9 +125,9 @@
    1.30  
    1.31  val command_kinds =
    1.32    [diag, document_heading, document_body, document_raw, thy_begin, thy_end, thy_load, thy_decl,
    1.33 -    thy_decl_block, thy_goal, qed, qed_script, qed_block, qed_global, prf_goal, prf_block,
    1.34 -    next_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script,
    1.35 -    prf_script_goal, prf_script_asm_goal];
    1.36 +    thy_decl_block, thy_defn, thy_stmt, thy_goal, thy_goal_defn, thy_goal_stmt, qed, qed_script,
    1.37 +    qed_block, qed_global, prf_goal, prf_block, next_block, prf_open, prf_close, prf_chain,
    1.38 +    prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal, prf_script_asm_goal];
    1.39  
    1.40  
    1.41  (* specifications *)
    1.42 @@ -256,10 +264,11 @@
    1.43  val is_theory_load = command_category [thy_load];
    1.44  
    1.45  val is_theory = command_category
    1.46 -  [thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_goal];
    1.47 +  [thy_begin, thy_end, thy_load, thy_decl, thy_decl_block, thy_defn, thy_stmt, thy_goal,
    1.48 +    thy_goal_defn, thy_goal_stmt];
    1.49  
    1.50  val is_theory_body = command_category
    1.51 -  [thy_load, thy_decl, thy_decl_block, thy_goal];
    1.52 +  [thy_load, thy_decl, thy_decl_block, thy_defn, thy_stmt, thy_goal, thy_goal_defn, thy_goal_stmt];
    1.53  
    1.54  val is_proof = command_category
    1.55    [qed, qed_script, qed_block, qed_global, prf_goal, prf_block, next_block, prf_open,
    1.56 @@ -271,7 +280,7 @@
    1.57      prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script, prf_script_goal,
    1.58      prf_script_asm_goal];
    1.59  
    1.60 -val is_theory_goal = command_category [thy_goal];
    1.61 +val is_theory_goal = command_category [thy_goal, thy_goal_defn, thy_goal_stmt];
    1.62  val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_script_goal, prf_script_asm_goal];
    1.63  val is_qed = command_category [qed, qed_script, qed_block];
    1.64  val is_qed_global = command_category [qed_global];