src/Pure/Interface/proof_general.ML
author wenzelm
Mon, 24 May 1999 21:54:34 +0200
changeset 6720 353bd9b74b1f
parent 6699 1471f2bd74a0
child 6724 b5007e5e8a1b
permissions -rw-r--r--
write_keywords generates outer syntax keyword classification in elisp;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
6699
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Interface/proof_general.ML
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
     3
    Author:     Markus Wenzel, TU Muenchen
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
     4
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
     5
Configuration for ProofGeneral of LFCS Edinburgh.
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
     6
*)
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
     7
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
     8
signature PROOF_GENERAL =
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
     9
sig
6720
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    10
  val write_keywords: string -> unit
6699
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    11
  val setup: (theory -> theory) list
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    12
  val init: bool -> unit
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    13
end;
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    14
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    15
structure ProofGeneral: PROOF_GENERAL =
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    16
struct
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    17
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    18
6720
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    19
(** generate keyword classification file **)
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    20
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    21
local
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    22
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    23
val regexp_meta = explode ".*+?[]^$";
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    24
val regexp_quote = implode o map (fn c => if c mem regexp_meta then "\\\\" ^ c else c) o explode;
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    25
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    26
fun defconst name strs =
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    27
  "\n(defconst isar-keywords-" ^ name ^
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    28
  "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    29
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    30
fun make_elisp_commands commands kind =
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    31
  defconst kind (mapfilter (fn (c, k) => if k = kind then Some c else None) commands);
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    32
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    33
fun make_elisp_syntax (keywords, commands) =
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    34
  ";;\n\
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    35
  \;; Keyword classification tables for Isabelle/Isar.\n\
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    36
  \;; This file generated by Isabelle -- DO NOT EDIT!\n\
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    37
  \;;\n\
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    38
  \;; $Id$\n\
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    39
  \;;\n" ^
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    40
  defconst "minor" (filter Syntax.is_identifier (keywords \\ map #1 commands)) ^
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    41
  implode (map (make_elisp_commands commands) OuterSyntax.Keyword.kinds) ^
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    42
  "\n(provide 'isar-keywords)\n";
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    43
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    44
in
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    45
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    46
fun write_keywords file =
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    47
  File.write (Path.unpack file) (make_elisp_syntax (OuterSyntax.dest_syntax ()));
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    48
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    49
end;
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    50
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    51
353bd9b74b1f write_keywords generates outer syntax keyword classification in elisp;
wenzelm
parents: 6699
diff changeset
    52
6699
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    53
(** compile-time theory setup **)
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    54
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    55
(* token translations *)
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    56
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    57
val proof_generalN = "ProofGeneral";
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    58
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    59
local
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    60
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    61
val end_tag = oct_char "350";
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    62
val tclass_tag = oct_char "351";
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    63
val tfree_tag = oct_char "352";
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    64
val tvar_tag = oct_char "353";
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    65
val free_tag = oct_char "354";
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    66
val bound_tag = oct_char "355";
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    67
val var_tag = oct_char "356";
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    68
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    69
fun tagit p x = (p ^ x ^ end_tag, real (size x));
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    70
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    71
in
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    72
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    73
val proof_general_trans =
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    74
 Syntax.tokentrans_mode proof_generalN
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    75
  [("class", tagit tclass_tag),
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    76
   ("tfree", tagit tfree_tag),
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    77
   ("tvar", tagit tvar_tag),
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    78
   ("free", tagit free_tag),
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    79
   ("bound", tagit bound_tag),
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    80
   ("var", tagit var_tag)];
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    81
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    82
end;
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    83
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    84
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    85
(* setup *)
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    86
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    87
val setup = [Theory.add_tokentrfuns proof_general_trans];
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    88
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    89
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    90
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    91
(** run-time initialization **)
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    92
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    93
(* messages *)
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    94
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    95
fun decorate_lines bg en "" = std_output o suffix "\n" o enclose bg en
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    96
  | decorate_lines bg en prfx = std_output o suffix "\n" o enclose bg en o prefix_lines prfx;
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    97
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    98
fun setup_messages () =
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
    99
 (writeln_fn := (decorate_lines (oct_char "360") (oct_char "361") "");
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   100
  warning_fn := (decorate_lines (oct_char "362") (oct_char "363") "### ");
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   101
  error_fn := (decorate_lines (oct_char "364") (oct_char "365") "*** "));
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   102
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   103
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   104
(* theory / proof state *)
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   105
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   106
fun setup_state () =
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   107
  (current_goals_markers :=
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   108
    let
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   109
      val begin_state = oct_char "366";
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   110
      val end_state= oct_char "367";
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   111
      val begin_goal = oct_char "370";
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   112
    in (begin_state, end_state, begin_goal) end;
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   113
  Toplevel.print_state_fn :=
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   114
    (Library.setmp writeln_fn (std_output o suffix "\n") Toplevel.print_state_default);
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   115
  Toplevel.prompt_state_fn := (suffix (oct_char "372") o Toplevel.prompt_state_default));
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   116
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   117
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   118
(* init *)
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   119
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   120
fun init isar =
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   121
 (setup_messages ();
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   122
  setup_state ();
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   123
  print_mode := [proof_generalN];
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   124
  set quick_and_dirty;
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   125
  if isar then Isar.main () else ());
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   126
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   127
1471f2bd74a0 Configuration for ProofGeneral of LFCS Edinburgh.
wenzelm
parents:
diff changeset
   128
end;