src/Pure/Isar/keyword.scala
author nipkow
Fri, 21 Jun 2013 09:00:26 +0200
changeset 52402 c2f30ba4bb98
parent 51274 cfc83ad52571
child 53371 47b23c582127
permissions -rw-r--r--
tuned
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
36947
285b39022372 renamed Outer_Keyword to Keyword (in Scala);
wenzelm
parents: 36681
diff changeset
     1
/*  Title:      Pure/Isar/keyword.scala
29449
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
     3
34158
8b66bd211dcf class Outer_Keyword wraps symbol interpretation, lexicon, keyword table;
wenzelm
parents: 32450
diff changeset
     4
Isar command keyword classification and keyword tables.
29449
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
     5
*/
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
     6
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
     7
package isabelle
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
     8
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
     9
36947
285b39022372 renamed Outer_Keyword to Keyword (in Scala);
wenzelm
parents: 36681
diff changeset
    10
object Keyword
32450
375db037f4d2 misc tuning;
wenzelm
parents: 29450
diff changeset
    11
{
36681
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    12
  /* kinds */
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    13
29449
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    14
  val MINOR = "minor"
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    15
  val CONTROL = "control"
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    16
  val DIAG = "diag"
46967
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    17
  val THY_BEGIN = "thy_begin"
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    18
  val THY_END = "thy_end"
46969
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46967
diff changeset
    19
  val THY_HEADING1 = "thy_heading1"
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46967
diff changeset
    20
  val THY_HEADING2 = "thy_heading2"
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46967
diff changeset
    21
  val THY_HEADING3 = "thy_heading3"
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46967
diff changeset
    22
  val THY_HEADING4 = "thy_heading4"
46967
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    23
  val THY_DECL = "thy_decl"
48867
e9beabf045ab some support for inlining file content into outer syntax token language;
wenzelm
parents: 46969
diff changeset
    24
  val THY_LOAD = "thy_load"
46967
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    25
  val THY_SCRIPT = "thy_script"
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    26
  val THY_GOAL = "thy_goal"
29449
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    27
  val QED = "qed"
46967
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    28
  val QED_BLOCK = "qed_block"
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    29
  val QED_GLOBAL = "qed_global"
46969
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46967
diff changeset
    30
  val PRF_HEADING2 = "prf_heading2"
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46967
diff changeset
    31
  val PRF_HEADING3 = "prf_heading3"
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46967
diff changeset
    32
  val PRF_HEADING4 = "prf_heading4"
46967
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    33
  val PRF_GOAL = "prf_goal"
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    34
  val PRF_BLOCK = "prf_block"
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    35
  val PRF_OPEN = "prf_open"
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    36
  val PRF_CLOSE = "prf_close"
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    37
  val PRF_CHAIN = "prf_chain"
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    38
  val PRF_DECL = "prf_decl"
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    39
  val PRF_ASM = "prf_asm"
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    40
  val PRF_ASM_GOAL = "prf_asm_goal"
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    41
  val PRF_SCRIPT = "prf_script"
29449
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    42
36681
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    43
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    44
  /* categories */
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    45
29449
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    46
  val minor = Set(MINOR)
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    47
  val control = Set(CONTROL)
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    48
  val diag = Set(DIAG)
40456
e91b3c2145b4 added missing Keyword.THY_SCHEMATIC_GOAL;
wenzelm
parents: 38236
diff changeset
    49
  val theory =
46969
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46967
diff changeset
    50
    Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
51274
cfc83ad52571 discontinued pointless command category "thy_schematic_goal" -- this is checked dynamically;
wenzelm
parents: 48867
diff changeset
    51
      THY_DECL, THY_SCRIPT, THY_GOAL)
46967
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    52
  val theory1 = Set(THY_BEGIN, THY_END)
29449
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    53
  val theory2 = Set(THY_DECL, THY_GOAL)
40456
e91b3c2145b4 added missing Keyword.THY_SCHEMATIC_GOAL;
wenzelm
parents: 38236
diff changeset
    54
  val proof =
46969
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46967
diff changeset
    55
    Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, PRF_GOAL,
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46967
diff changeset
    56
      PRF_BLOCK, PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_SCRIPT)
29450
ac7f67be7f1f tuned categories;
wenzelm
parents: 29449
diff changeset
    57
  val proof1 =
ac7f67be7f1f tuned categories;
wenzelm
parents: 29449
diff changeset
    58
    Set(QED, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL)
29449
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    59
  val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    60
  val improper = Set(THY_SCRIPT, PRF_SCRIPT)
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    61
}
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    62