# HG changeset patch
# User wenzelm
# Date 1414788520 -3600
# Node ID f8715e7c1be61bb03899ac5de03266f3ab5cc72e
# Parent  621c052789b42344ccb6b9db5ce7ec2d469a0f82
discontinued obsolete control command category;

diff -r 621c052789b4 -r f8715e7c1be6 src/Pure/Isar/keyword.ML
--- a/src/Pure/Isar/keyword.ML	Fri Oct 31 21:35:11 2014 +0100
+++ b/src/Pure/Isar/keyword.ML	Fri Oct 31 21:48:40 2014 +0100
@@ -9,7 +9,6 @@
   type T
   val kind_of: T -> string
   val kind_files_of: T -> string * string list
-  val control: T
   val diag: T
   val thy_begin: T
   val thy_end: T
@@ -56,8 +55,6 @@
   val dest: unit -> string list * string list
   val define: string * T option -> unit
   val is_diag: string -> bool
-  val is_control: string -> bool
-  val is_regular: string -> bool
   val is_heading: string -> bool
   val is_theory_begin: string -> bool
   val is_theory_load: string -> bool
@@ -92,7 +89,6 @@
 
 (* kinds *)
 
-val control = kind "control";
 val diag = kind "diag";
 val thy_begin = kind "thy_begin";
 val thy_end = kind "thy_end";
@@ -124,7 +120,7 @@
 val prf_script = kind "prf_script";
 
 val kinds =
-  [control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
+  [diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
     thy_load, thy_decl, thy_decl_block, thy_goal, qed, qed_script, 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_asm_goal_script, prf_script];
@@ -238,8 +234,6 @@
   end;
 
 val is_diag = command_category [diag];
-val is_control = command_category [control];
-val is_regular = not o command_category [diag, control];
 
 val is_heading =
   command_category [thy_heading1, thy_heading2, thy_heading3, thy_heading4,
diff -r 621c052789b4 -r f8715e7c1be6 src/Pure/Isar/keyword.scala
--- a/src/Pure/Isar/keyword.scala	Fri Oct 31 21:35:11 2014 +0100
+++ b/src/Pure/Isar/keyword.scala	Fri Oct 31 21:48:40 2014 +0100
@@ -12,7 +12,6 @@
   /* kinds */
 
   val MINOR = "minor"
-  val CONTROL = "control"
   val DIAG = "diag"
   val THY_BEGIN = "thy_begin"
   val THY_END = "thy_end"
@@ -46,7 +45,6 @@
   /* categories */
 
   val diag = Set(DIAG)
-  val control = Set(CONTROL)
 
   val heading = Set(THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
     PRF_HEADING2, PRF_HEADING3, PRF_HEADING4)
diff -r 621c052789b4 -r f8715e7c1be6 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Fri Oct 31 21:35:11 2014 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Fri Oct 31 21:48:40 2014 +0100
@@ -129,7 +129,7 @@
     val keywords1 = keywords + (name -> kind)
     val lexicon1 = lexicon + name
     val completion1 =
-      if (Keyword.control(kind._1) || replace == Some("")) completion
+      if (replace == Some("")) completion
       else completion + (name, replace getOrElse name)
     new Outer_Syntax(keywords1, lexicon1, completion1, language_context, true)
   }
diff -r 621c052789b4 -r f8715e7c1be6 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Fri Oct 31 21:35:11 2014 +0100
+++ b/src/Pure/PIDE/command.ML	Fri Oct 31 21:48:40 2014 +0100
@@ -162,10 +162,7 @@
     if is_malformed then Toplevel.malformed pos "Malformed command syntax"
     else
       (case Outer_Syntax.read_spans outer_syntax (resolve_files master_dir blobs span) of
-        [tr] =>
-          if Keyword.is_control (Toplevel.name_of tr) then
-            Toplevel.malformed pos "Illegal control command"
-          else Toplevel.modify_init init tr
+        [tr] => Toplevel.modify_init init tr
       | [] => Toplevel.ignored (#1 (Token.range_of span))
       | _ => Toplevel.malformed (#1 proper_range) "Exactly one command expected")
       handle ERROR msg => Toplevel.malformed (#1 proper_range) msg
diff -r 621c052789b4 -r f8715e7c1be6 src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Fri Oct 31 21:35:11 2014 +0100
+++ b/src/Pure/PIDE/markup.scala	Fri Oct 31 21:48:40 2014 +0100
@@ -264,7 +264,6 @@
   val VERBATIM = "verbatim"
   val CARTOUCHE = "cartouche"
   val COMMENT = "comment"
-  val CONTROL = "control"
 
 
   /* timing */