src/Pure/Isar/keyword.scala
author wenzelm
Fri, 01 Aug 2014 20:43:23 +0200
changeset 57837 63e3c45b85e1
parent 57836 7944e2588d1c
child 58800 bfed1c26caed
permissions -rw-r--r--
removed unused stuff;
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_GOAL = "thy_goal"
29449
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    26
  val QED = "qed"
53571
e58ca0311c0f more explicit indication of 'done' as proof script element;
wenzelm
parents: 53371
diff changeset
    27
  val QED_SCRIPT = "qed_script"
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"
53371
47b23c582127 more explicit indication of 'guess' as improper Isar (aka "script") element;
wenzelm
parents: 51274
diff changeset
    41
  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
    42
  val PRF_SCRIPT = "prf_script"
29449
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    43
36681
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    44
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    45
  /* categories */
dffeca08d3bf extractors for outer keyword declarations;
wenzelm
parents: 34166
diff changeset
    46
57835
43ff8638c02c more keyword categories (as in ML);
wenzelm
parents: 56146
diff changeset
    47
  val diag = Set(DIAG)
29449
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    48
  val control = Set(CONTROL)
57835
43ff8638c02c more keyword categories (as in ML);
wenzelm
parents: 56146
diff changeset
    49
43ff8638c02c more keyword categories (as in ML);
wenzelm
parents: 56146
diff changeset
    50
  val heading = Set(THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
43ff8638c02c more keyword categories (as in ML);
wenzelm
parents: 56146
diff changeset
    51
    PRF_HEADING2, PRF_HEADING3, PRF_HEADING4)
43ff8638c02c more keyword categories (as in ML);
wenzelm
parents: 56146
diff changeset
    52
40456
e91b3c2145b4 added missing Keyword.THY_SCHEMATIC_GOAL;
wenzelm
parents: 38236
diff changeset
    53
  val theory =
46969
481b7d9ad6fe more abstract heading level;
wenzelm
parents: 46967
diff changeset
    54
    Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
57836
7944e2588d1c agree on keyword categories with ML;
wenzelm
parents: 57835
diff changeset
    55
      THY_LOAD, THY_DECL, THY_GOAL)
57837
63e3c45b85e1 removed unused stuff;
wenzelm
parents: 57836
diff changeset
    56
57835
43ff8638c02c more keyword categories (as in ML);
wenzelm
parents: 56146
diff changeset
    57
  val theory_body =
43ff8638c02c more keyword categories (as in ML);
wenzelm
parents: 56146
diff changeset
    58
    Set(THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4, THY_LOAD, THY_DECL, THY_GOAL)
43ff8638c02c more keyword categories (as in ML);
wenzelm
parents: 56146
diff changeset
    59
40456
e91b3c2145b4 added missing Keyword.THY_SCHEMATIC_GOAL;
wenzelm
parents: 38236
diff changeset
    60
  val proof =
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_HEADING2, PRF_HEADING3, PRF_HEADING4,
57836
7944e2588d1c agree on keyword categories with ML;
wenzelm
parents: 57835
diff changeset
    62
      PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL,
7944e2588d1c agree on keyword categories with ML;
wenzelm
parents: 57835
diff changeset
    63
      PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
57835
43ff8638c02c more keyword categories (as in ML);
wenzelm
parents: 56146
diff changeset
    64
43ff8638c02c more keyword categories (as in ML);
wenzelm
parents: 56146
diff changeset
    65
  val proof_body =
43ff8638c02c more keyword categories (as in ML);
wenzelm
parents: 56146
diff changeset
    66
    Set(DIAG, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN,
43ff8638c02c more keyword categories (as in ML);
wenzelm
parents: 56146
diff changeset
    67
      PRF_DECL, PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
43ff8638c02c more keyword categories (as in ML);
wenzelm
parents: 56146
diff changeset
    68
43ff8638c02c more keyword categories (as in ML);
wenzelm
parents: 56146
diff changeset
    69
  val theory_goal = Set(THY_GOAL)
43ff8638c02c more keyword categories (as in ML);
wenzelm
parents: 56146
diff changeset
    70
  val proof_goal = Set(PRF_GOAL, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT)
43ff8638c02c more keyword categories (as in ML);
wenzelm
parents: 56146
diff changeset
    71
  val qed = Set(QED, QED_SCRIPT, QED_BLOCK)
43ff8638c02c more keyword categories (as in ML);
wenzelm
parents: 56146
diff changeset
    72
  val qed_global = Set(QED_GLOBAL)
29449
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    73
}
6e7745d35a30 added outer_keyword.scala: Isar command keyword classification;
wenzelm
parents:
diff changeset
    74