src/Pure/Isar/keyword.scala
author wenzelm
Wed, 11 Sep 2013 20:16:28 +0200
changeset 53571 e58ca0311c0f
parent 53371 47b23c582127
child 56146 8453d35e4684
permissions -rw-r--r--
more explicit indication of 'done' as proof script element;
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"
53571
e58ca0311c0f more explicit indication of 'done' as proof script element;
wenzelm
parents: 53371
diff changeset
    28
  val QED_SCRIPT = "qed_script"
46967
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    29
  val QED_BLOCK = "qed_block"
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    30
  val QED_GLOBAL = "qed_global"
46969
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46967
diff changeset
    31
  val PRF_HEADING2 = "prf_heading2"
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46967
diff changeset
    32
  val PRF_HEADING3 = "prf_heading3"
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46967
diff changeset
    33
  val PRF_HEADING4 = "prf_heading4"
46967
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    34
  val PRF_GOAL = "prf_goal"
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    35
  val PRF_BLOCK = "prf_block"
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    36
  val PRF_OPEN = "prf_open"
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    37
  val PRF_CLOSE = "prf_close"
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    38
  val PRF_CHAIN = "prf_chain"
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    39
  val PRF_DECL = "prf_decl"
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    40
  val PRF_ASM = "prf_asm"
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    41
  val PRF_ASM_GOAL = "prf_asm_goal"
53371
47b23c582127 more explicit indication of 'guess' as improper Isar (aka "script") element;
wenzelm
parents: 51274
diff changeset
    42
  val PRF_ASM_GOAL_SCRIPT = "prf_asm_goal_script"
46967
499d9bbd8de9 uniform keyword names within ML/Scala -- produce elisp names via external conversion;
wenzelm
parents: 46123
diff changeset
    43
  val PRF_SCRIPT = "prf_script"
29449
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    44
36681
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    45
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    46
  /* categories */
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    47
29449
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    48
  val minor = Set(MINOR)
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    49
  val control = Set(CONTROL)
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    50
  val diag = Set(DIAG)
40456
e91b3c2145b4 added missing Keyword.THY_SCHEMATIC_GOAL;
wenzelm
parents: 38236
diff changeset
    51
  val theory =
46969
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46967
diff changeset
    52
    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
    53
      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
    54
  val theory1 = Set(THY_BEGIN, THY_END)
29449
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    55
  val theory2 = Set(THY_DECL, THY_GOAL)
40456
e91b3c2145b4 added missing Keyword.THY_SCHEMATIC_GOAL;
wenzelm
parents: 38236
diff changeset
    56
  val proof =
53571
e58ca0311c0f more explicit indication of 'done' as proof script element;
wenzelm
parents: 53371
diff changeset
    57
    Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4,
e58ca0311c0f more explicit indication of 'done' as proof script element;
wenzelm
parents: 53371
diff changeset
    58
      PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL,
e58ca0311c0f more explicit indication of 'done' as proof script element;
wenzelm
parents: 53371
diff changeset
    59
      PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
29450
ac7f67be7f1f tuned categories;
wenzelm
parents: 29449
diff changeset
    60
  val proof1 =
53571
e58ca0311c0f more explicit indication of 'done' as proof script element;
wenzelm
parents: 53371
diff changeset
    61
    Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
e58ca0311c0f more explicit indication of 'done' as proof script element;
wenzelm
parents: 53371
diff changeset
    62
      PRF_CHAIN, PRF_DECL)
53371
47b23c582127 more explicit indication of 'guess' as improper Isar (aka "script") element;
wenzelm
parents: 51274
diff changeset
    63
  val proof2 = Set(PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
29449
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    64
  val improper = Set(THY_SCRIPT, PRF_SCRIPT)
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    65
}
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    66