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