discontinued obsolete control command category;
authorwenzelm
Fri Oct 31 21:48:40 2014 +0100 (2014-10-31 ago)
changeset 58853f8715e7c1be6
parent 58852 621c052789b4
child 58854 b979c781c2db
discontinued obsolete control command category;
src/Pure/Isar/keyword.ML
src/Pure/Isar/keyword.scala
src/Pure/Isar/outer_syntax.scala
src/Pure/PIDE/command.ML
src/Pure/PIDE/markup.scala
     1.1 --- a/src/Pure/Isar/keyword.ML	Fri Oct 31 21:35:11 2014 +0100
     1.2 +++ b/src/Pure/Isar/keyword.ML	Fri Oct 31 21:48:40 2014 +0100
     1.3 @@ -9,7 +9,6 @@
     1.4    type T
     1.5    val kind_of: T -> string
     1.6    val kind_files_of: T -> string * string list
     1.7 -  val control: T
     1.8    val diag: T
     1.9    val thy_begin: T
    1.10    val thy_end: T
    1.11 @@ -56,8 +55,6 @@
    1.12    val dest: unit -> string list * string list
    1.13    val define: string * T option -> unit
    1.14    val is_diag: string -> bool
    1.15 -  val is_control: string -> bool
    1.16 -  val is_regular: string -> bool
    1.17    val is_heading: string -> bool
    1.18    val is_theory_begin: string -> bool
    1.19    val is_theory_load: string -> bool
    1.20 @@ -92,7 +89,6 @@
    1.21  
    1.22  (* kinds *)
    1.23  
    1.24 -val control = kind "control";
    1.25  val diag = kind "diag";
    1.26  val thy_begin = kind "thy_begin";
    1.27  val thy_end = kind "thy_end";
    1.28 @@ -124,7 +120,7 @@
    1.29  val prf_script = kind "prf_script";
    1.30  
    1.31  val kinds =
    1.32 -  [control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
    1.33 +  [diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
    1.34      thy_load, thy_decl, thy_decl_block, thy_goal, qed, qed_script, qed_block, qed_global,
    1.35      prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open,
    1.36      prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
    1.37 @@ -238,8 +234,6 @@
    1.38    end;
    1.39  
    1.40  val is_diag = command_category [diag];
    1.41 -val is_control = command_category [control];
    1.42 -val is_regular = not o command_category [diag, control];
    1.43  
    1.44  val is_heading =
    1.45    command_category [thy_heading1, thy_heading2, thy_heading3, thy_heading4,
     2.1 --- a/src/Pure/Isar/keyword.scala	Fri Oct 31 21:35:11 2014 +0100
     2.2 +++ b/src/Pure/Isar/keyword.scala	Fri Oct 31 21:48:40 2014 +0100
     2.3 @@ -12,7 +12,6 @@
     2.4    /* kinds */
     2.5  
     2.6    val MINOR = "minor"
     2.7 -  val CONTROL = "control"
     2.8    val DIAG = "diag"
     2.9    val THY_BEGIN = "thy_begin"
    2.10    val THY_END = "thy_end"
    2.11 @@ -46,7 +45,6 @@
    2.12    /* categories */
    2.13  
    2.14    val diag = Set(DIAG)
    2.15 -  val control = Set(CONTROL)
    2.16  
    2.17    val heading = Set(THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
    2.18      PRF_HEADING2, PRF_HEADING3, PRF_HEADING4)
     3.1 --- a/src/Pure/Isar/outer_syntax.scala	Fri Oct 31 21:35:11 2014 +0100
     3.2 +++ b/src/Pure/Isar/outer_syntax.scala	Fri Oct 31 21:48:40 2014 +0100
     3.3 @@ -129,7 +129,7 @@
     3.4      val keywords1 = keywords + (name -> kind)
     3.5      val lexicon1 = lexicon + name
     3.6      val completion1 =
     3.7 -      if (Keyword.control(kind._1) || replace == Some("")) completion
     3.8 +      if (replace == Some("")) completion
     3.9        else completion + (name, replace getOrElse name)
    3.10      new Outer_Syntax(keywords1, lexicon1, completion1, language_context, true)
    3.11    }
     4.1 --- a/src/Pure/PIDE/command.ML	Fri Oct 31 21:35:11 2014 +0100
     4.2 +++ b/src/Pure/PIDE/command.ML	Fri Oct 31 21:48:40 2014 +0100
     4.3 @@ -162,10 +162,7 @@
     4.4      if is_malformed then Toplevel.malformed pos "Malformed command syntax"
     4.5      else
     4.6        (case Outer_Syntax.read_spans outer_syntax (resolve_files master_dir blobs span) of
     4.7 -        [tr] =>
     4.8 -          if Keyword.is_control (Toplevel.name_of tr) then
     4.9 -            Toplevel.malformed pos "Illegal control command"
    4.10 -          else Toplevel.modify_init init tr
    4.11 +        [tr] => Toplevel.modify_init init tr
    4.12        | [] => Toplevel.ignored (#1 (Token.range_of span))
    4.13        | _ => Toplevel.malformed (#1 proper_range) "Exactly one command expected")
    4.14        handle ERROR msg => Toplevel.malformed (#1 proper_range) msg
     5.1 --- a/src/Pure/PIDE/markup.scala	Fri Oct 31 21:35:11 2014 +0100
     5.2 +++ b/src/Pure/PIDE/markup.scala	Fri Oct 31 21:48:40 2014 +0100
     5.3 @@ -264,7 +264,6 @@
     5.4    val VERBATIM = "verbatim"
     5.5    val CARTOUCHE = "cartouche"
     5.6    val COMMENT = "comment"
     5.7 -  val CONTROL = "control"
     5.8  
     5.9  
    5.10    /* timing */