added outer_keyword.scala: Isar command keyword classification;
authorwenzelm
Sun Jan 11 20:40:09 2009 +0100 (2009-01-11)
changeset 294496e7745d35a30
parent 29448 34b9652b2f45
child 29450 ac7f67be7f1f
added outer_keyword.scala: Isar command keyword classification;
src/Pure/IsaMakefile
src/Pure/Isar/outer_keyword.scala
     1.1 --- a/src/Pure/IsaMakefile	Sun Jan 11 18:18:35 2009 +0100
     1.2 +++ b/src/Pure/IsaMakefile	Sun Jan 11 20:40:09 2009 +0100
     1.3 @@ -26,37 +26,37 @@
     1.4    Concurrent/par_list_dummy.ML Concurrent/simple_thread.ML		\
     1.5    Concurrent/synchronized.ML Concurrent/task_queue.ML General/ROOT.ML	\
     1.6    General/alist.ML General/balanced_tree.ML General/basics.ML		\
     1.7 -  General/binding.ML							\
     1.8 -  General/buffer.ML General/file.ML General/graph.ML General/heap.ML	\
     1.9 -  General/integer.ML General/lazy.ML General/markup.ML			\
    1.10 -  General/name_space.ML General/ord_list.ML General/output.ML		\
    1.11 -  General/path.ML General/position.ML General/pretty.ML			\
    1.12 -  General/print_mode.ML General/properties.ML General/queue.ML		\
    1.13 -  General/scan.ML General/secure.ML General/seq.ML General/source.ML	\
    1.14 -  General/stack.ML General/symbol.ML General/symbol_pos.ML		\
    1.15 -  General/table.ML General/url.ML General/xml.ML General/yxml.ML	\
    1.16 -  Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML Isar/attrib.ML		\
    1.17 -  Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML Isar/class_target.ML Isar/code.ML	\
    1.18 -  Isar/code_unit.ML Isar/constdefs.ML Isar/context_rules.ML		\
    1.19 -  Isar/element.ML Isar/expression.ML Isar/find_theorems.ML		\
    1.20 -  Isar/isar.ML Isar/isar_cmd.ML Isar/isar_syn.ML	\
    1.21 -  Isar/local_defs.ML Isar/local_syntax.ML Isar/local_theory.ML		\
    1.22 -  Isar/locale.ML Isar/method.ML Isar/net_rules.ML Isar/old_locale.ML	\
    1.23 +  General/binding.ML General/buffer.ML General/file.ML			\
    1.24 +  General/graph.ML General/heap.ML General/integer.ML General/lazy.ML	\
    1.25 +  General/markup.ML General/name_space.ML General/ord_list.ML		\
    1.26 +  General/output.ML General/path.ML General/position.ML			\
    1.27 +  General/pretty.ML General/print_mode.ML General/properties.ML		\
    1.28 +  General/queue.ML General/scan.ML General/secure.ML General/seq.ML	\
    1.29 +  General/source.ML General/stack.ML General/symbol.ML			\
    1.30 +  General/symbol_pos.ML General/table.ML General/url.ML General/xml.ML	\
    1.31 +  General/yxml.ML Isar/ROOT.ML Isar/antiquote.ML Isar/args.ML		\
    1.32 +  Isar/attrib.ML Isar/auto_bind.ML Isar/calculation.ML Isar/class.ML	\
    1.33 +  Isar/class_target.ML Isar/code.ML Isar/code_unit.ML			\
    1.34 +  Isar/constdefs.ML Isar/context_rules.ML Isar/element.ML		\
    1.35 +  Isar/expression.ML Isar/find_theorems.ML Isar/isar.ML			\
    1.36 +  Isar/isar_cmd.ML Isar/isar_syn.ML Isar/local_defs.ML			\
    1.37 +  Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML		\
    1.38 +  Isar/method.ML Isar/net_rules.ML Isar/old_locale.ML			\
    1.39    Isar/object_logic.ML Isar/obtain.ML Isar/outer_keyword.ML		\
    1.40    Isar/outer_lex.ML Isar/outer_parse.ML Isar/outer_syntax.ML		\
    1.41    Isar/overloading.ML Isar/proof.ML Isar/proof_context.ML		\
    1.42    Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML		\
    1.43    Isar/rule_insts.ML Isar/session.ML Isar/skip_proof.ML			\
    1.44 -  Isar/spec_parse.ML Isar/specification.ML		\
    1.45 -  Isar/theory_target.ML Isar/toplevel.ML Isar/value_parse.ML		\
    1.46 -  ML-Systems/alice.ML ML-Systems/exn.ML					\
    1.47 -  ML-Systems/install_pp_polyml.ML ML-Systems/ml_name_space.ML		\
    1.48 -  ML-Systems/multithreading.ML ML-Systems/mosml.ML			\
    1.49 -  ML-Systems/multithreading_polyml.ML ML-Systems/overloading_smlnj.ML	\
    1.50 -  ML-Systems/polyml-4.1.3.ML ML-Systems/polyml-4.1.4.ML			\
    1.51 -  ML-Systems/polyml-4.2.0.ML ML-Systems/polyml-5.0.ML			\
    1.52 -  ML-Systems/polyml-5.1.ML ML-Systems/polyml_common.ML			\
    1.53 -  ML-Systems/polyml.ML ML-Systems/polyml_old_compiler4.ML		\
    1.54 +  Isar/spec_parse.ML Isar/specification.ML Isar/theory_target.ML	\
    1.55 +  Isar/toplevel.ML Isar/value_parse.ML ML-Systems/alice.ML		\
    1.56 +  ML-Systems/exn.ML ML-Systems/install_pp_polyml.ML			\
    1.57 +  ML-Systems/ml_name_space.ML ML-Systems/multithreading.ML		\
    1.58 +  ML-Systems/mosml.ML ML-Systems/multithreading_polyml.ML		\
    1.59 +  ML-Systems/overloading_smlnj.ML ML-Systems/polyml-4.1.3.ML		\
    1.60 +  ML-Systems/polyml-4.1.4.ML ML-Systems/polyml-4.2.0.ML			\
    1.61 +  ML-Systems/polyml-5.0.ML ML-Systems/polyml-5.1.ML			\
    1.62 +  ML-Systems/polyml_common.ML ML-Systems/polyml.ML			\
    1.63 +  ML-Systems/polyml_old_compiler4.ML					\
    1.64    ML-Systems/polyml_old_compiler5.ML ML-Systems/proper_int.ML		\
    1.65    ML-Systems/smlnj.ML ML-Systems/system_shell.ML			\
    1.66    ML-Systems/time_limit.ML ML-Systems/thread_dummy.ML			\
    1.67 @@ -126,8 +126,9 @@
    1.68  SCALA_FILES = General/event_bus.scala General/markup.scala		\
    1.69    General/position.scala General/swing.scala General/symbol.scala	\
    1.70    General/xml.scala General/yxml.scala Isar/isar.scala			\
    1.71 -  Thy/thy_header.scala Tools/isabelle_process.scala			\
    1.72 -  Tools/isabelle_syntax.scala Tools/isabelle_system.scala
    1.73 +  Isar/outer_keyword.scala Thy/thy_header.scala				\
    1.74 +  Tools/isabelle_process.scala Tools/isabelle_syntax.scala		\
    1.75 +  Tools/isabelle_system.scala
    1.76  
    1.77  
    1.78  SCALA_TARGET = $(ISABELLE_HOME)/lib/classes/Pure.jar
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/Pure/Isar/outer_keyword.scala	Sun Jan 11 20:40:09 2009 +0100
     2.3 @@ -0,0 +1,46 @@
     2.4 +/*  Title:      Pure/Isar/outer_keyword.scala
     2.5 +    Author:     Makarius
     2.6 +
     2.7 +Isar command keyword classification.
     2.8 +*/
     2.9 +
    2.10 +package isabelle
    2.11 +
    2.12 +object OuterKeyword {
    2.13 +
    2.14 +  val MINOR = "minor"
    2.15 +  val CONTROL = "control"
    2.16 +  val DIAG = "diag"
    2.17 +  val THY_BEGIN = "theory-begin"
    2.18 +  val THY_SWITCH = "theory-switch"
    2.19 +  val THY_END = "theory-end"
    2.20 +  val THY_HEADING = "theory-heading"
    2.21 +  val THY_DECL = "theory-decl"
    2.22 +  val THY_SCRIPT = "theory-script"
    2.23 +  val THY_GOAL = "theory-goal"
    2.24 +  val QED = "qed"
    2.25 +  val QED_BLOCK = "qed-block"
    2.26 +  val QED_GLOBAL = "qed-global"
    2.27 +  val PRF_HEADING = "proof-heading"
    2.28 +  val PRF_GOAL = "proof-goal"
    2.29 +  val PRF_BLOCK = "proof-block"
    2.30 +  val PRF_OPEN = "proof-open"
    2.31 +  val PRF_CLOSE = "proof-close"
    2.32 +  val PRF_CHAIN = "proof-chain"
    2.33 +  val PRF_DECL = "proof-decl"
    2.34 +  val PRF_ASM = "proof-asm"
    2.35 +  val PRF_ASM_GOAL = "proof-asm-goal"
    2.36 +  val PRF_SCRIPT = "proof-script"
    2.37 +
    2.38 +  val minor = Set(MINOR)
    2.39 +  val control = Set(CONTROL)
    2.40 +  val diag = Set(DIAG)
    2.41 +  val theory0 = Set(THY_BEGIN, THY_SWITCH, THY_END)
    2.42 +  val theory1 = Set(THY_HEADING)
    2.43 +  val theory2 = Set(THY_DECL, THY_GOAL)
    2.44 +  val proof1 = Set(QED, QED_BLOCK, QED_GLOBAL, PRF_HEADING, PRF_GOAL, PRF_BLOCK, PRF_OPEN,
    2.45 +    PRF_CLOSE, PRF_CHAIN, PRF_DECL)
    2.46 +  val proof2 = Set(PRF_ASM, PRF_ASM_GOAL)
    2.47 +  val improper = Set(THY_SCRIPT, PRF_SCRIPT)
    2.48 +}
    2.49 +