src/Pure/proof_general.ML
author aspinall
Wed, 18 Aug 2004 16:25:27 +0200
changeset 15145 07360eef9f4f
parent 15134 d3fa5e1d6e4d
child 15146 eab7de0d0a31
permissions -rw-r--r--
Version for PGIP 2.X, with greatly improved parsing and XML handling.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12780
6b41c750451c tuned title;
wenzelm
parents: 12778
diff changeset
     1
(*  Title:      Pure/proof_general.ML
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
     2
    ID:         $Id$
14675
08b9c690f9cf removed obsolete 'undo';
wenzelm
parents: 14568
diff changeset
     3
    Author:     David Aspinall and Markus Wenzel
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
     4
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
     5
Isabelle configuration for Proof General (see http://proofgeneral.inf.ed.ac.uk)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
     6
Includes support for PGIP control language for Isabelle/Isar.
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
     7
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
     8
===========================================================================
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
     9
NOTE: With this version you will lose support for the Isabelle
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    10
preferences menu in the currently released version of Proof General (3.5).
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    11
No other changes should be visible in the Emacs interface.
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    12
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    13
If the loss of preferences is a serious problem, please use a "sticky"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    14
check-out of the previous version of this file, version 1.27.
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    15
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
    16
A version of Emacs Proof General which supports the new PGIP format for
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    17
preferences will be available shortly.  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    18
===========================================================================
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    19
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
    20
STATUS: this version is an experimental version that supports PGIP 2.X.
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    21
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    22
*)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    23
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    24
signature PROOF_GENERAL =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    25
sig
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    26
  val setup: (theory -> theory) list
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    27
  val update_thy_only: string -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    28
  val try_update_thy_only: string -> unit
13391
553e7b62680f fixed inform_file_retracted: remove_thy;
wenzelm
parents: 13284
diff changeset
    29
  val inform_file_retracted: string -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    30
  val inform_file_processed: string -> unit
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    31
  val preferences: 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    32
      (string * 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    33
	(string * 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    34
	 (string * 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    35
	  (string * (string * (unit -> string)) * 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    36
	   (string -> unit)))) list) list ref
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
    37
  val process_pgip: string -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    38
  val thms_containing: string list -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    39
  val help: unit -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    40
  val show_context: unit -> theory
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    41
  val kill_goal: unit -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    42
  val repeat_undo: int -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    43
  val isa_restart: unit -> unit
12833
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
    44
  val full_proofs: bool -> unit
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    45
  val isarcmd: string -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    46
  val init: bool -> unit
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    47
  val init_pgip: bool -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    48
  val write_keywords: string -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    49
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    50
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    51
structure ProofGeneral : PROOF_GENERAL =
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    52
struct
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    53
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
    54
structure P = OuterParse
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
    55
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    56
(* PGIP messaging mode (independent of PGML output) *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    57
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    58
val pgip_active = ref false;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    59
val pgip_emacs_compatibility_flag = ref false;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    60
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    61
fun pgip () = (!pgip_active);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    62
fun pgip_emacs_compatibility () = (!pgip_emacs_compatibility_flag);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    63
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    64
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    65
(* print modes *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    66
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    67
val proof_generalN = "ProofGeneral"; (* token markup (colouring vars, etc.) *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    68
val xsymbolsN = Symbol.xsymbolsN;    (* XSymbols symbols *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    69
val pgmlN = "PGML";		     (* XML escapes and PGML symbol elements *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    70
val pgmlatomsN = "PGMLatoms";	     (* variable kind decorations *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    71
val thm_depsN = "thm_deps";	     (* meta-information about theorem deps *)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    72
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    73
fun pgml () = pgmlN mem_string ! print_mode;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    74
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    75
(* text output: print modes for xsymbol and PGML *)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    76
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    77
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    78
14827
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    79
fun xsym_output "\\" = "\\\\"
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    80
  | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    81
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    82
fun xsymbols_output s =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    83
  if xsymbolsN mem_string ! print_mode andalso exists_string (equal "\\") s then
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    84
    let val syms = Symbol.explode s
14827
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    85
    in (implode (map xsym_output syms), real (Symbol.length syms)) end
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    86
  else Symbol.default_output s;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    87
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    88
fun pgml_sym s =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    89
  (case Symbol.decode s of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    90
    Symbol.Char "\\" => "\\\\"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    91
  | Symbol.Char s => XML.text s
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    92
  | Symbol.Sym s => XML.element "sym" [("name", s)] []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    93
  | Symbol.Ctrl s => XML.element "ctrl" [("name", s)] []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    94
  | Symbol.Raw s => s);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    95
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    96
fun pgml_output str =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    97
  let val syms = Symbol.explode str
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    98
  in (implode (map pgml_sym syms), real (Symbol.length syms)) end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    99
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   100
in 
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   101
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   102
fun setup_xsymbols_output () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   103
    Output.add_mode 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   104
	xsymbolsN 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   105
	(xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   106
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   107
fun setup_pgml_output () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   108
    Output.add_mode 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   109
	pgmlN
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   110
	(pgml_output, Symbol.default_indent, Symbol.encode_raw);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   111
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   112
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   113
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   114
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   115
(* token translations *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   116
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   117
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   118
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   119
val end_tag = oct_char "350";
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   120
val class_tag = ("class", oct_char "351");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   121
val tfree_tag = ("tfree", oct_char "352");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   122
val tvar_tag = ("tvar", oct_char "353");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   123
val free_tag = ("free", oct_char "354");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   124
val bound_tag = ("bound", oct_char "355");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   125
val var_tag = ("var", oct_char "356");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   126
val skolem_tag = ("skolem", oct_char "357");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   127
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   128
fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   129
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   130
fun tagit (kind, bg_tag) x =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   131
    (if Output.has_mode pgmlatomsN then 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   132
	 xml_atom kind x
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   133
     else bg_tag ^ x ^ end_tag, 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   134
     real (Symbol.length (Symbol.explode x)));
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   135
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   136
fun free_or_skolem x =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   137
  (case try Syntax.dest_skolem x of
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   138
    None => tagit free_tag x
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   139
  | Some x' => tagit skolem_tag x');
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   140
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   141
fun var_or_skolem s =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   142
  (case Syntax.read_var s of
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   143
    Var ((x, i), _) =>
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   144
      (case try Syntax.dest_skolem x of
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   145
        None => tagit var_tag s
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   146
      | Some x' => tagit skolem_tag (Syntax.string_of_vname (x', i)))
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   147
  | _ => tagit var_tag s);
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   148
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   149
val proof_general_trans =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   150
 Syntax.tokentrans_mode proof_generalN
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   151
  [("class", tagit class_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   152
   ("tfree", tagit tfree_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   153
   ("tvar", tagit tvar_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   154
   ("free", free_or_skolem),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   155
   ("bound", tagit bound_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   156
   ("var", var_or_skolem)];
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   157
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   158
in val setup = [Theory.add_tokentrfuns proof_general_trans] end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   159
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   160
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   161
(* assembling PGIP packets *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   162
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   163
val pgip_refseq = ref None : string option ref
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   164
val pgip_refid = ref None : string option ref
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   165
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   166
local
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   167
    val myseq_no = ref 1;      (* PGIP packet counter *)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   168
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   169
    val pgip_class  = "pg"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   170
    val pgip_origin = "Isabelle/Isar"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   171
    val pgip_id = (getenv "HOSTNAME") ^ "/" ^ (getenv "USER") ^ "/" ^ 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   172
		   (Time.toString(Time.now()))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   173
	          (* FIXME: PPID is empty for me: any way to get process ID? *)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   174
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   175
    fun assemble_pgips pgips = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   176
	XML.element 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   177
	     "pgip" 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   178
	     ([("class",  pgip_class),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   179
	       ("origin", pgip_origin),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   180
	       ("id",     pgip_id)] @
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   181
	      (if_none (apsome (single o (pair "refseq")) (!pgip_refseq)) []) @
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   182
	      (if_none (apsome (single o (pair "refid")) (!pgip_refid)) []) @
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   183
	      [("seq",  string_of_int (Library.inc myseq_no))])
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   184
	     pgips
13526
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   185
in
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   186
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   187
 fun decorated_output bg en prfx = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   188
    writeln_default o enclose bg en o prefix_lines prfx;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   189
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   190
 (* FIXME: see Rev 1.48 [PG CVS] for cleaner version of this which can be used
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   191
    for PG 4.0 which processes PGIP without needing special chars. *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   192
 fun issue_pgips ps = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   193
     if pgip_emacs_compatibility() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   194
	 decorated_output (* add urgent message annotation *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   195
	     (oct_char "360") (oct_char "361") "" 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   196
	     (assemble_pgips ps)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   197
     else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   198
	 writeln_default (assemble_pgips ps)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   199
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   200
 fun assemble_pgip resp attrs s = assemble_pgips [XML.element resp attrs [s]]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   201
				  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   202
 fun assemble_pgipe resp attrs = assemble_pgips [XML.element resp attrs []]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   203
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   204
 (* FIXME: need to add stuff to gather PGIPs here *)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   205
 fun issue_pgip resp attrs = writeln_default o (assemble_pgip resp attrs)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   206
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   207
(*  FIXME: temporarily to support PG 3.4.  *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   208
 fun issue_pgip_maybe_decorated bg en resp attrs s = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   209
     if pgip_emacs_compatibility() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   210
      (*  in PGIP mode, but using escape characters as well.  *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   211
	writeln_default (enclose bg en (assemble_pgip resp attrs s))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   212
     else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   213
	issue_pgip resp attrs s
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   214
	
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   215
 fun issue_pgipe resp attrs = writeln_default (assemble_pgipe resp attrs)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   216
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   217
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   218
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   219
(* messages and notification *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   220
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   221
fun message resp attrs bg en prfx s =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   222
  if pgip() then 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   223
      issue_pgip_maybe_decorated bg en resp attrs (prefix_lines prfx s)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   224
  else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   225
      decorated_output bg en prfx s;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   226
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   227
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   228
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   229
    val display_area = ("area", "display")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   230
    val message_area = ("area", "message")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   231
    val tracing_category = ("category", "tracing")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   232
    val urgent_indication = ("urgent", "y")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   233
    val nonfatal = ("fatality", "nonfatal")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   234
    val fatal = ("fatality", "fatal")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   235
    val panic = ("fatality", "panic")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   236
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   237
    val thyname_attr = pair "thyname"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   238
    val url_attr = pair "url"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   239
    fun localfile_url_attr path = url_attr ("file:///" ^ path)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   240
in			   
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   241
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   242
fun setup_messages () =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   243
 (writeln_fn  := message "normalresponse" [message_area] "" "" "";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   244
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   245
  priority_fn := message "normalresponse" [message_area, urgent_indication]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   246
			 (oct_char "360") (oct_char "361") "";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   247
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   248
  tracing_fn := message "normalresponse"  [message_area, tracing_category]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   249
			(oct_char "360" ^ oct_char "375") (oct_char "361") "";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   250
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   251
  warning_fn := message "errorresponse"    [nonfatal]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   252
			(oct_char "362") (oct_char "363") "### ";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   253
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   254
  error_fn := message "errorresponse" [fatal]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   255
		      (oct_char "364") (oct_char "365") "*** ";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   256
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   257
  panic_fn := message "errorresponse" [panic]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   258
		      (oct_char "364") (oct_char "365") "!!! ")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   259
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   260
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   261
(* accumulate printed output in a single PGIP response *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   262
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   263
fun with_displaywrap (elt,attrs) dispfn =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   264
    let 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   265
	val lines = ref ([] : string list);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   266
	fun wlgrablines s = (lines:= (s :: (!lines)))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   267
    in 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   268
	(setmp writeln_fn wlgrablines dispfn ();
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   269
	 (* FIXME: cat_lines here inefficient, should use stream output *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   270
         issue_pgip elt attrs (cat_lines (!lines)))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   271
    end
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   272
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   273
val emacs_notify = decorated_output (oct_char "360") (oct_char "361") "";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   274
    
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   275
fun tell_clear_goals () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   276
    if pgip() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   277
	issue_pgipe "cleardisplay" [display_area]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   278
    else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   279
	emacs_notify "Proof General, please clear the goals buffer.";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   280
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   281
fun tell_clear_response () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   282
    if pgip() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   283
	issue_pgipe "cleardisplay" [message_area]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   284
    else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   285
	emacs_notify "Proof General, please clear the response buffer.";
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   286
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   287
fun tell_file_loaded path = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   288
    if pgip() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   289
	issue_pgipe "informtheoryloaded"  (* FIXME: get thy name from info here? *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   290
		    [thyname_attr        (XML.text (File.sysify_path path)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   291
		     localfile_url_attr  (XML.text (File.sysify_path path))]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   292
    else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   293
	emacs_notify ("Proof General, this file is loaded: " 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   294
		      ^ quote (File.sysify_path path));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   295
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   296
fun tell_file_retracted path = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   297
    if pgip() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   298
	issue_pgipe "informtheoryretracted"  (* FIXME: get thy name from info here? *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   299
		    [thyname_attr        (XML.text (File.sysify_path path)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   300
		     localfile_url_attr  (XML.text (File.sysify_path path))]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   301
    else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   302
	emacs_notify ("Proof General, you can unlock the file " 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   303
		      ^ quote (File.sysify_path path));
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   304
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   305
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   306
(* theory / proof state output *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   307
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   308
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   309
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   310
    fun tmp_markers f =	setmp Display.current_goals_markers 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   311
			      (oct_char "366", oct_char "367", "") f ()
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   312
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   313
    fun statedisplay prts =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   314
	issue_pgip "proofstate" []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   315
		   (XML.element "pgml" []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   316
				[XML.element "statedisplay" 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   317
					     [] 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   318
					     [Output.output (* FIXME: needed? *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   319
						  (Pretty.output
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   320
						       (Pretty.chunks prts))]])
13545
fcdbd6cf5f9f improved tell_thm_deps;
wenzelm
parents: 13538
diff changeset
   321
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   322
    fun print_current_goals n m st =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   323
	if pgml () then statedisplay (Display.pretty_current_goals n m st)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   324
	else tmp_markers (fn () => Display.print_current_goals_default n m st)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   325
	     
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   326
    fun print_state b st =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   327
	if pgml () then statedisplay (Toplevel.pretty_state b st)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   328
	else tmp_markers (fn () => Toplevel.print_state_default b st)
13526
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   329
in
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   330
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   331
 fun setup_state () =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   332
     (Display.print_current_goals_fn := print_current_goals;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   333
      Toplevel.print_state_fn := print_state;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   334
      (* FIXME: check next octal char won't appear in pgip? *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   335
      Toplevel.prompt_state_fn := (suffix (oct_char "372") o  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   336
				   Toplevel.prompt_state_default));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   337
end
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   338
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   339
end
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   340
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   341
(* misc commands for ProofGeneral/isa *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   342
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   343
fun thms_containing ss =
13284
20c818c966e6 thms_containing: optional limit argument;
wenzelm
parents: 13273
diff changeset
   344
  ProofContext.print_thms_containing (ProofContext.init (the_context ())) None ss;
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   345
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   346
val welcome = priority o Session.welcome;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   347
val help = welcome;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   348
val show_context = Context.the_context;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   349
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   350
fun kill_goal () = (Goals.reset_goals (); tell_clear_goals ());
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   351
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   352
fun no_print_goals f = setmp Display.print_current_goals_fn (fn _ => fn _ => fn _ => ()) f;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   353
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   354
fun repeat_undo 0 = ()
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   355
  | repeat_undo 1 = undo ()
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   356
  | repeat_undo n = (no_print_goals undo (); repeat_undo (n - 1));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   357
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   358
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   359
(* theory loader actions *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   360
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   361
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   362
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   363
fun add_master_files name files =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   364
  let val masters = [ThyLoad.thy_path name, ThyLoad.ml_path name]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   365
  in masters @ gen_rems (op = o pairself Path.base) (files, masters) end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   366
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   367
fun trace_action action name =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   368
  if action = ThyInfo.Update then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   369
    seq tell_file_loaded (ThyInfo.loaded_files name)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   370
  else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   371
    seq tell_file_retracted (add_master_files name (ThyInfo.loaded_files name))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   372
  else ();
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   373
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   374
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   375
  fun setup_thy_loader () = ThyInfo.add_hook trace_action;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   376
  fun sync_thy_loader () = seq (trace_action ThyInfo.Update) (ThyInfo.names ());
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   377
end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   378
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   379
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   380
(* prepare theory context *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   381
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   382
val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   383
val update_thy_only = setmp MetaSimplifier.trace_simp 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   384
			    false ThyInfo.update_thy_only;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   385
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   386
fun which_context () =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   387
  (case Context.get_context () of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   388
    Some thy => "  Using current (dynamic!) one: " ^
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   389
      (case try PureThy.get_name thy of Some name => quote name | None => "<unnamed>")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   390
  | None => "");
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   391
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   392
fun try_update_thy_only file =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   393
  ThyLoad.cond_add_path (Path.dir (Path.unpack file)) (fn () =>
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   394
    let val name = thy_name file in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   395
      if is_some (ThyLoad.check_file (ThyLoad.thy_path name)) 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   396
      then update_thy_only name
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   397
      else warning ("Unkown theory context of ML file." ^ which_context ())
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   398
    end) ();
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   399
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   400
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   401
(* get informed about files *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   402
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   403
val inform_file_retracted = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   404
    ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   405
val inform_file_processed = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   406
    ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   407
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   408
fun proper_inform_file_processed file state =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   409
  let val name = thy_name file in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   410
    if Toplevel.is_toplevel state andalso ThyInfo.known_thy name then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   411
     (ThyInfo.touch_child_thys name;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   412
      transform_error ThyInfo.pretend_use_thy_only name handle ERROR_MESSAGE msg =>
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   413
       (warning msg; warning ("Failed to register theory: " ^ quote name);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   414
        tell_file_retracted (Path.base (Path.unpack file))))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   415
    else raise Toplevel.UNDEF
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   416
  end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   417
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   418
fun vacuous_inform_file_processed file state =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   419
 (warning ("No theory " ^ quote (thy_name file));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   420
  tell_file_retracted (Path.base (Path.unpack file)));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   421
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   422
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   423
(* restart top-level loop (keeps most state information) *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   424
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   425
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   426
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   427
fun restart isar =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   428
 (if isar then tell_clear_goals () else kill_goal ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   429
  tell_clear_response ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   430
  welcome ());
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   431
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   432
in
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   433
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   434
fun isa_restart () = restart false;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   435
fun isar_restart () = (sync_thy_loader (); restart true; raise Toplevel.RESTART);
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   436
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   437
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   438
12833
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   439
fun full_proofs true = proofs := 2
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   440
  | full_proofs false = proofs := 1;
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   441
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   442
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   443
(* theorem dependency output *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   444
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   445
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   446
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   447
val spaces_quote = space_implode " " o map quote;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   448
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   449
fun thm_deps_message (thms, deps) = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   450
    if pgip() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   451
	issue_pgips 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   452
	    [XML.element
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   453
		 "metainforesponse"  (* FIXME: get thy name from info here? *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   454
		 [("infotype", "isabelle_theorem_dependencies")]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   455
		 [XML.element "value" [("name", "thms")] [XML.text thms],
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   456
		  XML.element "value" [("name", "deps")] [XML.text deps]]]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   457
    else emacs_notify 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   458
	     ("Proof General, theorem dependencies of " 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   459
	      ^ thms ^ " are " ^ deps)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   460
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   461
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   462
fun tell_thm_deps ths =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   463
  conditional (thm_depsN mem_string ! print_mode) (fn () =>
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   464
    let
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   465
      val names = map Thm.name_of_thm ths \ "";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   466
      val deps = Symtab.keys (foldl (uncurry Proofterm.thms_of_proof)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   467
				    (Symtab.empty, map Thm.proof_of ths)) \ "";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   468
    in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   469
      if null names orelse null deps then ()
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   470
      else thm_deps_message (spaces_quote names, spaces_quote deps)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   471
    end);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   472
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   473
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   474
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   475
fun setup_present_hook () =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   476
  Present.add_hook (fn _ => fn res => tell_thm_deps (flat (map #2 res)));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   477
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   478
end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   479
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   480
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   481
(*** Preferences ***)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   482
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   483
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   484
val pgipnat        = XML.element "pgipint" [("min", "0")] [] 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   485
fun pgipnatmax max = XML.element "pgipint" [("min", "0"), 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   486
					    ("max", string_of_int max)] []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   487
val pgipbool       = XML.element "pgipbool" [] []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   488
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   489
fun withdefault f = (f(), f)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   490
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   491
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   492
fun nat_option r = (pgipnat,
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   493
  withdefault (fn () => string_of_int (!r)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   494
  (fn s => (case Syntax.read_nat s of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   495
       None => error "nat_option: illegal value"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   496
     | Some i => r := i)));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   497
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   498
fun bool_option r = (pgipbool,
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   499
  withdefault (fn () => Bool.toString (!r)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   500
  (fn "false" => r := false | "true" => r := true
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   501
    | _ => error "bool_option: illegal value"));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   502
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   503
val proof_option = (pgipbool,
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   504
  withdefault (fn () => Bool.toString (!proofs >= 2)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   505
  (fn "false" => proofs := 1 | "true" => proofs := 2
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   506
    | _ => error "proof_option: illegal value"));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   507
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   508
val thm_deps_option = (pgipbool,
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   509
  withdefault (fn () => Bool.toString (Output.has_mode "thm_deps")),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   510
  (fn "false" => print_mode := ((!print_mode) \ "thm_deps")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   511
    | "true" => print_mode := ("thm_deps" ins (!print_mode))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   512
    | _ => error "thm_deps_option: illegal value"));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   513
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   514
local 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   515
    val pg_print_depth_val = ref 10
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   516
    fun pg_print_depth n = (print_depth n; pg_print_depth_val := n)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   517
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   518
val print_depth_option = (pgipnat,
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   519
  withdefault (fn () => string_of_int (!pg_print_depth_val)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   520
  (fn s => (case Syntax.read_nat s of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   521
       None => error "print_depth_option: illegal value"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   522
     | Some i => pg_print_depth i)))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   523
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   524
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   525
val preferences = ref 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   526
  [("Display",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   527
    [("show-types", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   528
      ("Include types in display of Isabelle terms", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   529
       bool_option show_types)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   530
     ("show-sorts", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   531
      ("Include sorts in display of Isabelle terms", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   532
       bool_option show_sorts)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   533
     ("show-consts", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   534
      ("Show types of consts in Isabelle goal display",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   535
       bool_option show_consts)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   536
     ("long-names", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   537
      ("Show fully qualified names in Isabelle terms", bool_option long_names)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   538
     ("show-brackets", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   539
      ("Show full bracketing in Isabelle terms",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   540
       bool_option show_brackets)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   541
     ("show-main-goal", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   542
      ("Show main goal in proof state display", bool_option Proof.show_main_goal)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   543
     ("eta-contract", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   544
      ("Print terms eta-contracted",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   545
       bool_option Syntax.eta_contract))]),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   546
   ("Advanced Display",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   547
    [("goals-limit", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   548
      ("Setting for maximum number of goals printed",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   549
       nat_option goals_limit)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   550
     ("prems-limit", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   551
      ("Setting for maximum number of premises printed",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   552
       nat_option ProofContext.prems_limit)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   553
     ("print-depth", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   554
      ("Setting for the ML print depth",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   555
       print_depth_option))]),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   556
   ("Tracing",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   557
    [("trace-simplifier", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   558
      ("Trace simplification rules.",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   559
       bool_option trace_simp)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   560
     ("trace-rules", ("Trace application of the standard rules",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   561
		      bool_option trace_rules)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   562
     ("trace-unification", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   563
      ("Output error diagnostics during unification",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   564
       bool_option Pattern.trace_unify_fail)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   565
     ("global-timing", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   566
      ("Whether to enable timing in Isabelle.",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   567
       bool_option Output.timing))]),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   568
   ("Proof", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   569
    [("quick-and-dirty", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   570
      ("Take a few (interactive-only) short cuts",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   571
       bool_option quick_and_dirty)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   572
     ("full-proofs", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   573
      ("Record full proof objects internally",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   574
       proof_option)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   575
     ("theorem-dependencies", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   576
       ("Track theorem dependencies within Proof General",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   577
	thm_deps_option))])
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   578
   ];
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   579
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   580
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   581
(* Configuration: GUI config, proverinfo messages *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   582
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   583
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   584
    val config_file = "~~/lib/ProofGeneral/pgip_isar.xml"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   585
    val name_attr = pair "name"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   586
    val version_attr = pair "version"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   587
    val isabelle_www = "http://isabelle.in.tum.de/"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   588
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   589
fun send_pgip_config () =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   590
    let 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   591
	val path = Path.unpack config_file
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   592
	val exists = File.exists path
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   593
	val proverinfo = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   594
	    XML.element "proverinfo"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   595
              [("name",Session.name()), ("version", version),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   596
	       ("url", isabelle_www)]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   597
	    [XML.element "welcomemsg" [] [XML.text (Session.welcome())],
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   598
	     XML.element "helpdoc" 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   599
         (* NB: would be nice to generate/display docs from isatool
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   600
          doc, but that program may not be running on same machine;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   601
          front end should be responsible for launching viewer, etc. *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   602
		      [("name", "Isabelle/HOL Tutorial"),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   603
		       ("descr", "A Gentle Introduction to Isabelle/HOL"), 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   604
		       ("url",  "http://isabelle.in.tum.de/dist/Isabelle2003/doc/tutorial.pdf")]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   605
	      []]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   606
    in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   607
	if exists then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   608
	    (issue_pgips [proverinfo]; issue_pgips [File.read path])
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   609
	else panic ("PGIP configuration file " ^ config_file ^ " not found")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   610
    end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   611
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   612
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   613
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   614
(* PGIP identifier tables (prover objects). [incomplete] *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   615
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   616
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   617
    val objtype_thy  = "theory"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   618
    val objtype_thm  = "theorem"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   619
    val objtype_term = "term"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   620
    val objtype_type = "type"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   621
		       
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   622
    fun xml_idtable ty ctx ids = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   623
	let
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   624
            fun ctx_attr (Some c)= [("context", c)]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   625
              | ctx_attr None    = []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   626
	    fun xmlid x = XML.element "identifier" [] [XML.text x];
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   627
	in 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   628
	    XML.element "idtable" (("objtype", ty)::ctx_attr ctx)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   629
	                          (map xmlid ids)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   630
	end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   631
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   632
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   633
fun setids t = issue_pgip "setids" [] t
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   634
fun addids t = issue_pgip "addids" [] t
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   635
fun delids t = issue_pgip "delids" [] t
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   636
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   637
fun delallids ty = setids (xml_idtable ty None [])
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   638
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   639
fun send_thy_idtable ctx thys = setids (xml_idtable objtype_thy ctx thys)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   640
fun clear_thy_idtable () = delallids objtype_thy
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   641
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   642
fun send_thm_idtable ctx thy = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   643
    addids (xml_idtable objtype_thm ctx (map fst (PureThy.thms_of thy)));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   644
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   645
fun clear_thm_idtable () = delallids objtype_thm
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   646
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   647
(* fun send_type_idtable thy = TODO, it's a bit low-level messy
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   648
   & maybe not so useful anyway *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   649
	
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   650
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   651
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   652
(* Response to interface queries about known objects *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   653
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   654
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   655
 val topthy = Toplevel.theory_of o Toplevel.get_state
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   656
 val pthm = print_thm oo get_thm
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   657
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   658
 fun idvalue tp nm = ("idvalue",[("objtype",tp),("name",nm)])
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   659
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   660
fun askids (None, Some "theory")  = send_thy_idtable None (ThyInfo.names())
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   661
  | askids (None, None) =  send_thy_idtable None (ThyInfo.names())
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   662
                           (* only theories known in top context *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   663
  | askids (Some thy, Some "theory") = send_thy_idtable (Some thy) (ThyInfo.get_preds thy)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   664
  | askids (Some thy, Some "theorem") = send_thm_idtable (Some thy) (ThyInfo.get_theory thy)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   665
  | askids (Some thy, None) = (send_thy_idtable (Some thy) (ThyInfo.get_preds thy);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   666
                               send_thm_idtable (Some thy) (ThyInfo.get_theory thy)) 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   667
  | askids (_, Some ot) = error ("No objects of type "^(quote ot)^" are available here.")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   668
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   669
fun showid (_,        "theory", n) = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   670
    with_displaywrap (idvalue "theory" n) (fn ()=>(print_theory (ThyInfo.get_theory n)))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   671
  | showid (Some thy, "theorem", t) = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   672
    with_displaywrap (idvalue "theorem" t) (fn ()=>(pthm (ThyInfo.get_theory thy) t))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   673
  | showid (None,     "theorem", t) = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   674
    with_displaywrap (idvalue "theorem" t) (fn ()=>pthm (topthy()) t)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   675
  | showid (_, ot, _) = error ("Cannot show objects of type "^ot)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   676
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   677
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   678
	 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   679
(** Parsing proof scripts without execution **)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   680
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   681
local
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   682
    fun markup_text str elt = [XML.element elt [] [XML.text str]]
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   683
    fun markup_text_attrs str elt attrs = [XML.element elt attrs [XML.text str]]
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   684
    fun empty elt = [XML.element elt [] []]
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   685
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   686
    fun named_item_elt toks str elt nameP objtyp = 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   687
	let 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   688
	    val name = (fst (nameP toks))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   689
			handle _ => (error ("Error occurred in name parser for " ^ elt);
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   690
				     "")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   691
				     
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   692
	in 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   693
	    [XML.element elt 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   694
			 ((if name="" then [] else [("name", name)])@
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   695
			  (if objtyp="" then [] else [("objtype", objtyp)]))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   696
			 ([XML.text str])]
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   697
	end
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   698
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   699
    fun parse_warning msg = warning ("script->PGIP markup parser: " ^ msg)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   700
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   701
    (* FIXME: allow dynamic extensions to language here: we need a hook in
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   702
       outer_syntax.ML to reset this table. *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   703
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   704
    val keywords_classification_table = ref (None:(string Symtab.table) option)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   705
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   706
    fun get_keywords_classification_table () = 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   707
	case (!keywords_classification_table) of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   708
	    Some t => t
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   709
	  | None => (let
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   710
			 val tab = foldl (fn (tab,(c,_,k,_))=>Symtab.update((c,k),tab)) 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   711
					 (Symtab.empty,OuterSyntax.dest_parsers())
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   712
		     in (keywords_classification_table := Some tab; tab) end)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   713
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   714
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   715
		    
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   716
    fun xmls_of_thy_begin (name,toks,str) = (* see isar_syn.ML/theoryP *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   717
	let 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   718
	    val ((thyname,imports,files),_) = ThyHeader.args toks
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   719
	in 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   720
	    markup_text_attrs str "opentheory" [("thyname",thyname)]
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   721
	end 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   722
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   723
    fun xmls_of_thy_decl (name,toks,str) = (* see isar_syn.ML/thy_decl cases  *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   724
	let 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   725
	    (* NB: PGIP only deals with single name bindings at the moment;
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   726
	       potentially we could markup grouped definitions several times but
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   727
	       that might suggest the wrong structure to the editor?
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   728
	       Better alternative would be to put naming closer around text,
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   729
	       but to do that we'd be much better off modifying the real parser
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   730
	       instead of reconstructing it here. *)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   731
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   732
	    val plain_items = (* no names, unimportant names, or too difficult *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   733
		["defaultsort","arities","judgement","finalconsts",
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   734
		 "syntax", "nonterminals", "translations",
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   735
		 "global", "local", "hide",
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   736
		 "ML_setup", "setup", "method_setup",
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   737
		 "parse_ast_translation", "parse_translation", "print_translation",
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   738
		 "typed_print_translation", "print_ast_translation", "token_translation",
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   739
		 "oracle",
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   740
		 "declare"]
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   741
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   742
	    val plain_item   = markup_text str "theoryitem"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   743
	    val comment_item = markup_text str "litcomment"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   744
	    val named_item   = named_item_elt toks str "theoryitem"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   745
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   746
	    val opt_overloaded = P.opt_keyword "overloaded";
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   747
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   748
	    val thmnameP = (* see isar_syn.ML/theoremsP *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   749
		let 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   750
		    val name_facts = P.and_list1 ((P.opt_thm_name "=" --| P.xthms1) >> #1)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   751
		    val theoremsP = P.locale_target |-- name_facts >> (fn [] => "" | x::_ => x)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   752
		in 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   753
		    theoremsP
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   754
		end
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   755
	in 
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   756
	    if (name mem plain_items) then plain_item
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   757
	    else case name of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   758
		     "text"      => comment_item
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   759
		   | "text_raw"  => comment_item
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   760
		   | "typedecl"  => named_item (P.type_args |-- P.name) "type"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   761
		   | "types"     => named_item (P.type_args |-- P.name) "type"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   762
		   | "classes"   => named_item P.name "class"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   763
		   | "classrel"  => named_item P.name "class"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   764
		   | "consts"    => named_item (P.const >> #1) "term"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   765
		   | "axioms"    => named_item (P.spec_name >> (#1 o #1)) "theorem"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   766
		   | "defs"	 => named_item (opt_overloaded |-- P.spec_name >> (#1 o #1)) "theorem"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   767
		   | "constdefs" => named_item P.name (* FIXME: heavily simplified/wrong *) "term"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   768
		   | "theorems"  => named_item thmnameP "thmset"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   769
		   | "lemmas"    => named_item thmnameP "thmset"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   770
		   | "oracle"    => named_item P.name "oracle"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   771
		   | "locale"	 => named_item ((P.opt_keyword "open" >> not) |-- P.name) "locale"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   772
		   | _ => (parse_warning ("Unrecognized thy-decl command: " ^ name); plain_item)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   773
	end
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   774
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   775
    fun xmls_of_thy_goal (name,toks,str) = 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   776
	let 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   777
	    val nameP = P.locale_target |-- ((P.opt_thm_name ":") >> #1)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   778
	    (* TODO: add preference values for attributes 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   779
	       val prefval = XML.element "prefval" [("name","thm-kind"),("value",name)]
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   780
	    *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   781
	in 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   782
	    named_item_elt toks str "opengoal" nameP ""
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   783
	end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   784
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   785
    fun xmls_of_qed (name,markup) = case name of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   786
      "sorry"         => markup "giveupgoal"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   787
    | "oops"          => markup "postponegoal"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   788
    | "done"          => markup "closegoal" 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   789
    | "by"            => markup "closegoal"  (* nested or toplevel *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   790
    | "qed"           => markup "closegoal"  (* nested or toplevel *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   791
    | "."	      => markup "closegoal"  (* nested or toplevel *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   792
    | ".."	      => markup "closegoal"  (* nested or toplevel *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   793
    | other => (* default to closegoal: may be wrong for extns *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   794
      (parse_warning ("Unrecognized qed command: " ^ quote other); markup "closegoal")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   795
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   796
    fun xmls_of_kind kind (name,toks,str) = 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   797
    let val markup = markup_text str in 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   798
    case kind of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   799
      "control"        => markup "badcmd"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   800
    | "diag"           => markup "spuriouscmd"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   801
    (* theory/files *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   802
    | "theory-begin"   => xmls_of_thy_begin (name,toks,str)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   803
    | "theory-decl"    => xmls_of_thy_decl (name,toks,str)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   804
    | "theory-heading" => markup "litcomment"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   805
    | "theory-script"  => markup "theorystep"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   806
    (* proof control *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   807
    | "theory-goal"    => xmls_of_thy_goal (name,toks,str)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   808
    | "proof-heading"  => markup "litcomment"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   809
    | "proof-goal"     => markup "opengoal"  (* nested proof: have, show, ... *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   810
    | "proof-block"    => markup "proofstep" (* context-shift: proof, next; really "newgoal" *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   811
    | "proof-open"     => (empty "openblock") @ (markup "proofstep")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   812
    | "proof-close"    => (markup "proofstep") @ (empty "closeblock")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   813
    | "proof-script"   => markup "proofstep"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   814
    | "proof-chain"    => markup "proofstep"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   815
    | "proof-decl"     => markup "proofstep"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   816
    | "proof-asm"      => markup "proofstep"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   817
    | "proof-asm-goal" => markup "proofstep"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   818
    | "qed"            => xmls_of_qed (name,markup)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   819
    | "qed-block"      => xmls_of_qed (name,markup)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   820
    | "qed-global"     => xmls_of_qed (name,markup)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   821
    | other => (* default for anything else is "spuriouscmd", ignored for undo. *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   822
      (parse_warning ("Internal inconsistency, unrecognized keyword kind: " ^ quote other);
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   823
       markup "spuriouscmd")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   824
    end 
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   825
in
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   826
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   827
fun xmls_of_transition (name,str,toks) = 
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   828
   let 
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   829
       val classification = Symtab.lookup (get_keywords_classification_table(),name)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   830
   in case classification of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   831
	  Some k => (xmls_of_kind k (name,toks,str))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   832
	| None => (* an uncategorized keyword ignored for undo (maybe wrong) *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   833
	  (parse_warning ("Uncategorized command found: " ^ name ^ " -- using spuriouscmd");
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   834
	   markup_text str "spuriouscmd")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   835
   end 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   836
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   837
fun xmls_of_impropers [] = []
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   838
  | xmls_of_impropers toks = 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   839
    let 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   840
	val (whs,rest) = take_prefix (not o OuterLex.is_proper) toks
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   841
	fun markup [] _ = []
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   842
	  | markup toks x = markup_text (implode (map OuterLex.unparse toks)) x
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   843
    in
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   844
	(markup whs "comment") @ (markup rest "unparseable")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   845
    end
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   846
    
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   847
end
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   848
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   849
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   850
local
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   851
    (* we have to weave together the whitespace/comments with proper tokens 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   852
       to reconstruct the input. *)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   853
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   854
    fun match_tokens ([],us,vs) = (rev vs,us)  (* used, unused *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   855
      | match_tokens (t::ts,w::ws,vs) = 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   856
	if (t = w) then match_tokens (ts,ws,w::vs)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   857
	else match_tokens (t::ts,ws,w::vs)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   858
      | match_tokens _ = error ("match_tokens: mismatched input parse")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   859
in
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   860
    fun xmls_of_str str =
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   861
    let 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   862
       val toks = OuterSyntax.scan str
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   863
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   864
       (* parsing:   See outer_syntax.ML/toplevel_source *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   865
    
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   866
       fun parse_loop ([],[],xmls) = xmls
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   867
	 | parse_loop ([],itoks,xmls) = xmls @ (xmls_of_impropers itoks)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   868
	 | parse_loop ((nm,toks,_)::trs,itoks,xmls) =
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   869
	   let 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   870
	       (* first proper token is command, except FIXME for -- *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   871
	       val (prewhs,cmditoks') = take_prefix (not o OuterLex.is_proper) itoks
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   872
	       val (cmdtok,itoks') = case cmditoks' of x::xs => (x,xs)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   873
						  | _ => error("proof_general/parse_loop impossible") 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   874
	       val (utoks,itoks'') = match_tokens (toks,itoks',[])
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   875
               (* FIXME: should take trailing [w/s+] semicolon too in utoks *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   876
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   877
	       val str = implode (map OuterLex.unparse (cmdtok::utoks))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   878
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   879
	       val xmls_whs = xmls_of_impropers prewhs 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   880
	       val xmls_tr  = xmls_of_transition (nm,str,toks)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   881
	   in
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   882
	       parse_loop(trs,itoks'',xmls @ xmls_whs @ xmls_tr)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   883
	   end
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   884
    in
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   885
	(* FIXME: put errors/warnings inside the parse result *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   886
	parse_loop (OuterSyntax.read toks, toks, [])
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   887
    end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   888
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   889
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   890
fun parsescript str = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   891
    issue_pgips [XML.element "parseresult" [] (xmls_of_str str)]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   892
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   893
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   894
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   895
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   896
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   897
(**** PGIP:  Isabelle -> Interface ****)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   898
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   899
val isabelle_pgml_version_supported = "1.0"; 
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   900
val isabelle_pgip_version_supported = "2.0"
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   901
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   902
fun usespgip () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   903
    issue_pgipe "usespgip" [("version", isabelle_pgip_version_supported)];
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   904
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   905
fun usespgml () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   906
    issue_pgipe "usespgml" [("version", isabelle_pgml_version_supported)];
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   907
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   908
fun hasprefs () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   909
    seq (fn (prefcat, prefs) =>
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   910
	    issue_pgips [XML.element "hasprefs" [("prefcategory",prefcat)]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   911
		 (map (fn (name, (descr, (ty, (default,_),_))) => 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   912
		       XML.element "haspref" [("name", name), 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   913
					      ("descr", descr), 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   914
					      ("default", default)]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   915
		       [ty]) prefs)]) (!preferences);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   916
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   917
fun allprefs () = foldl (op @) ([], map snd (!preferences))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   918
	
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   919
fun setpref name value = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   920
    (case assoc (allprefs(), name) of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   921
	 None => warning ("Unknown pref: " ^ quote name)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   922
       | Some (_, (_, _, set)) => set value);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   923
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   924
fun getpref name = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   925
    (case assoc (allprefs(), name) of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   926
	 None => warning ("Unknown pref: " ^ quote name)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   927
       | Some (_, (_, (_,get), _)) => 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   928
	   issue_pgip "prefval" [("name", name)] (get ()));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   929
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   930
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   931
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   932
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   933
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   934
(**** PGIP:  Interface -> Isabelle/Isar ****)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   935
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   936
exception PGIP of string;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   937
exception PGIP_QUIT;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   938
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   939
(* Sending commands to Isar *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   940
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   941
fun isarcmd s = 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   942
    s |> OuterSyntax.scan |> OuterSyntax.read 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   943
      |> map (Toplevel.position (Position.name "PGIP message") o #3) |> Toplevel.>>>;
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   944
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   945
fun xmltext ((XML.Text text)::ts) = text ^ (xmltext ts)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   946
  | xmltext [] = ""
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   947
  | xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   948
			
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   949
fun isarscript xmls = isarcmd (xmltext xmls)   (* send a script command *)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   950
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   951
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   952
(* load an arbitrary (.thy or .ML) file *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   953
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   954
fun use_thy_or_ml_file file = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   955
    let
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   956
	val (path,extn) = Path.split_ext (Path.unpack file)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   957
    in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   958
	case extn of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   959
	    "" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   960
	  | "thy" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   961
	  | "ML" => isarcmd ("use " ^ quote file)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   962
	  (* instead of error we could guess theory? *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   963
	  | other => error ("Don't know how to read a file with extension " ^ other)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   964
    end  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   965
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   966
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   967
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   968
  (* Proof control commands *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   969
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   970
  fun xmlattro attrs attr = assoc(attrs,attr)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   971
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   972
  fun xmlattr attrs attr = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   973
      (case xmlattro attrs attr of 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   974
	   Some value => value 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   975
	 | None => raise PGIP ("Missing attribute: " ^ attr))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   976
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   977
  val thyname_attr = "thyname"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   978
  val objtype_attr = "objtype"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   979
  val name_attr = "name"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   980
  val dirname_attr = "dir"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   981
  fun comment x = "(* " ^ x ^ " *)"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   982
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   983
  (* parse URLs like "file://host/name.thy" *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   984
  (* FIXME: instead of this, extend code in General/url.ML & use that. *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   985
  fun decode_url url = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   986
      (let 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   987
	  val sep = find_index_eq ":" (explode url)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   988
 	  val proto = String.substring(url,0,sep)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   989
	  val hostsep = find_index_eq "/" (drop (sep+3,explode url))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   990
	  val host = String.substring(url,sep+3,hostsep-sep+4)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   991
	  val doc = if (size url >= sep+hostsep+3) then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   992
			String.substring(url,sep+hostsep+4,size url-hostsep-sep-4) 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   993
		    else ""
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   994
      in 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   995
	  (proto,host,doc)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   996
      end) handle Subscript => error ("Badly formed URL " ^ url)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   997
 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   998
  fun localfile_of_url url =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   999
      let
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1000
	  val (proto,host,name) = decode_url url
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1001
      in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1002
	  if (proto = "file" andalso 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1003
	      (host = "" orelse 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1004
	       host = "localhost" orelse 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1005
	       host = (getenv "HOSTNAME")))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1006
	     then name
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1007
	  else error ("Cannot access non-local URL " ^ url)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1008
      end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1009
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1010
  fun fileurl_of attrs = localfile_of_url (xmlattr attrs "url")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1011
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1012
  val topthy = Toplevel.theory_of o Toplevel.get_state
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1013
  val topthy_name = PureThy.get_name o topthy
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1014
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1015
  val currently_open_file = ref (None : string option)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1016
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1017
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1018
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1019
fun process_pgip_element pgipxml = (case pgipxml of 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1020
  (XML.Text t) => warning ("Ignored text in PGIP packet: \n" ^ t)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1021
| (XML.Elem (xml as (elem, attrs, data))) => 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1022
  (case elem of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1023
       (* protocol config *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1024
       "askpgip"  	=> (usespgip (); send_pgip_config ())
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1025
     | "askpgml"  	=> usespgml ()
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1026
     (* proverconfig *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1027
     | "askprefs" 	=> hasprefs ()
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1028
     | "getpref"  	=> getpref (xmlattr attrs name_attr)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1029
     | "setpref"  	=> setpref (xmlattr attrs name_attr) (xmltext data)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1030
     (* provercontrol *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1031
     | "proverinit" 	=> isar_restart ()
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1032
     | "proverexit" 	=> isarcmd "quit"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1033
     | "startquiet" 	=> isarcmd "disable_pr"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1034
     | "stopquiet"  	=> isarcmd "enable_pr"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1035
     | "pgmlsymbolson"   => (print_mode := (["xsymbols", "symbols"] @ ! print_mode))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1036
     | "pgmlsymbolsoff"  => (print_mode := (Library.gen_rems 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1037
						(op =) 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1038
						(! print_mode, ["xsymbols", "symbols"])))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1039
     (* properproofcmd: proper commands which belong in script *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1040
     | "opengoal"       => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1041
     | "proofstep"      => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1042
     | "closegoal"      => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1043
     | "giveupgoal"     => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1044
     | "postponegoal"   => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1045
     | "comment"	=> isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1046
     | "litcomment"     => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1047
     | "spuriouscmd"    => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1048
     | "badcmd"		=> isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1049
     (* improperproofcmd: improper commands which *do not* belong in script *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1050
     | "undostep"       => isarcmd "ProofGeneral.undo"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1051
     | "abortgoal"      => isarcmd "ProofGeneral.kill_proof"  
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1052
     | "forget"         => error "Not implemented" 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1053
     | "restoregoal"    => error "Not implemented"  (* could just treat as forget? *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1054
     (* proofctxt: improper commands *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1055
     | "askids"         => askids (xmlattro attrs thyname_attr, 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1056
				   xmlattro attrs objtype_attr)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1057
     | "showid"	        => showid (xmlattro attrs thyname_attr, 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1058
				   xmlattr attrs objtype_attr,
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1059
		     		   xmlattr attrs name_attr)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1060
     | "parsescript"    => parsescript (xmltext data)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1061
     | "showproofstate" => isarcmd "pr"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1062
     | "showctxt"       => isarcmd "print_theory"   (* more useful than print_context *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1063
     | "searchtheorems" => isarcmd ("thms_containing " ^ (xmltext data))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1064
     | "setlinewidth"   => isarcmd ("pretty_setmargin " ^ (xmltext data))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1065
     | "viewdoc"	=> isarcmd ("print_" ^ (xmltext data)) (* FIXME: isatool doc? *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1066
     (* properfilecmd: proper theory-level script commands *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1067
     | "opentheory"     => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1068
     | "theoryitem"     => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1069
     | "closetheory"    => (isarscript data;
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1070
			    writeln ("Theory "^(topthy_name())^" completed."))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1071
     (* improperfilecmd: theory-level commands not in script *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1072
     | "aborttheory"    => isarcmd ("init_toplevel")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1073
     | "retracttheory"  => isarcmd ("kill_thy " ^
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1074
				    (quote (xmlattr attrs thyname_attr)))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1075
     | "loadfile"       => use_thy_or_ml_file    (fileurl_of attrs)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1076
     | "openfile"       => (inform_file_retracted (fileurl_of attrs);
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1077
			    currently_open_file := Some (fileurl_of attrs))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1078
     | "closefile"      => (case !currently_open_file of 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1079
				Some f => (inform_file_processed f;
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1080
					   currently_open_file := None)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1081
			      | None => raise PGIP ("closefile when no file is open!"))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1082
     | "abortfile"      => (currently_open_file := None) (* perhaps error for no file open *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1083
     | "changecwd"      => ThyLoad.add_path (xmlattr attrs dirname_attr)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1084
     (* unofficial command for debugging *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1085
     | "quitpgip" => raise PGIP_QUIT  
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1086
     | _ => raise PGIP ("Unrecognized PGIP element: " ^ elem)))
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1087
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1088
fun process_pgip_tree s = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1089
    (pgip_refseq := None; 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1090
     pgip_refid := None;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1091
     (case s of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1092
	  XML.Elem ("pgip", attrs, pgips) => 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1093
	  (let 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1094
	       val class = xmlattr attrs "class"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1095
	       val _ = (pgip_refseq := xmlattro attrs "seq";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1096
			pgip_refid :=  xmlattro attrs "id")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1097
	   in  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1098
	       if (class = "pa") then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1099
		   seq process_pgip_element pgips
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1100
	       else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1101
		   raise PGIP "PGIP packet for me should have class=\"pa\""
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1102
	   end)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1103
	| _ => raise PGIP "Invalid PGIP packet received") 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1104
     handle (PGIP msg) => 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1105
	    (error (msg ^ "\nPGIP error occured in XML text below:\n" ^ 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1106
		    (XML.string_of_tree s))))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1107
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1108
(* for export to Emacs *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1109
(* val process_pgip = process_pgip_tree o XML.tree_of_string; *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1110
(* FIXME: for temporary compatibility with PG 3.4, we engage special characters
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1111
   during output *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1112
fun process_pgip s = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1113
    (pgip_emacs_compatibility_flag := true;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1114
     process_pgip_tree (XML.tree_of_string s);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1115
     pgip_emacs_compatibility_flag := false)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1116
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1117
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1118
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1119
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1120
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1121
(* PGIP loop: process PGIP input only *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1122
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1123
local  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1124
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1125
exception XML_PARSE
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1126
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1127
fun loop src : unit =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1128
    let 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1129
	val _ = issue_pgipe "ready" []
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1130
	val pgipo = (Source.get_single src) 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1131
			handle e => raise XML_PARSE
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1132
    in
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1133
	case pgipo of  
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1134
	     None  => ()
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1135
	   | Some (pgip,src') =>  
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1136
	     ((process_pgip_tree pgip); loop src') handle e => handler (e,Some src')
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1137
    end handle e => handler (e,Some src)  (* i.e. error in ready/XML parse *)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1138
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1139
and handler (e,srco) = 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1140
    case (e,srco) of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1141
        (XML_PARSE,Some src) => 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1142
	(* (!error_fn "Invalid XML input, aborting"; ()) NB: loop OK for tty, but want exit on EOF *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1143
         panic "Invalid XML input, aborting"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1144
      | (PGIP_QUIT,_) => ()
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1145
      | (ERROR,Some src) => loop src (* message already given *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1146
      | (Interrupt,Some src) => (!error_fn "Interrupt during PGIP processing"; loop src)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1147
      | (Toplevel.UNDEF,Some src) => (error "No working context defined"; loop src) (* usually *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1148
      | (e,Some src) => (error (Toplevel.exn_message e); loop src)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1149
      | (_,None) => ()
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1150
in
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1151
  (* NB: simple tty for now; later might read from other tty-style sources (e.g. sockets). *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1152
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1153
  val xmlP = XML.scan_comment_whspc |-- XML.parse_elem >> single
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1154
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1155
  val tty_src = Source.set_prompt "" (Source.source Symbol.stopper xmlP None Source.tty)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1156
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1157
  val pgip_toplevel =  loop 
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1158
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1159
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1160
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1161
(* additional outer syntax for Isar *)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1162
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1163
local structure P = OuterParse and K = OuterSyntax.Keyword in
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1164
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1165
val undoP = (* undo without output *)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1166
  OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1167
    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1168
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1169
val context_thy_onlyP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1170
  OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1171
    (P.name >> (Toplevel.no_timing oo IsarThy.init_context update_thy_only));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1172
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1173
val try_context_thy_onlyP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1174
  OuterSyntax.improper_command "ProofGeneral.try_context_thy_only" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1175
    (P.name >> (Toplevel.no_timing oo
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1176
      (Toplevel.imperative (K ()) oo IsarThy.init_context try_update_thy_only)));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1177
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1178
val restartP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1179
  OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1180
    (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative isar_restart)));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1181
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1182
val kill_proofP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1183
  OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1184
    (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1185
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1186
val inform_file_processedP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1187
  OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control
14902
bef0dc694c48 Path.split_ext; more robust inform_file_processed;
wenzelm
parents: 14880
diff changeset
  1188
    (P.name >> (fn file => Toplevel.no_timing o
bef0dc694c48 Path.split_ext; more robust inform_file_processed;
wenzelm
parents: 14880
diff changeset
  1189
      Toplevel.keep (vacuous_inform_file_processed file) o
bef0dc694c48 Path.split_ext; more robust inform_file_processed;
wenzelm
parents: 14880
diff changeset
  1190
      Toplevel.kill o
bef0dc694c48 Path.split_ext; more robust inform_file_processed;
wenzelm
parents: 14880
diff changeset
  1191
      Toplevel.keep (proper_inform_file_processed file)));
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1192
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1193
val inform_file_retractedP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1194
  OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1195
    (P.name >> (Toplevel.no_timing oo
14902
bef0dc694c48 Path.split_ext; more robust inform_file_processed;
wenzelm
parents: 14880
diff changeset
  1196
      (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1197
14725
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
  1198
val process_pgipP =
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
  1199
  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
  1200
    (P.text >> (Toplevel.no_timing oo
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
  1201
      (fn txt => Toplevel.imperative (fn () => process_pgip txt))));
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
  1202
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1203
fun init_outer_syntax () = OuterSyntax.add_parsers
14675
08b9c690f9cf removed obsolete 'undo';
wenzelm
parents: 14568
diff changeset
  1204
 [undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
14725
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
  1205
  inform_file_processedP, inform_file_retractedP, process_pgipP];
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1206
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1207
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1208
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1209
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1210
(* init *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1211
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1212
val initialized = ref false;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1213
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1214
fun set_prompts true _ = ml_prompts "ML> " "ML# " 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1215
  | set_prompts false true = ml_prompts "PGIP-ML>" "PGIP-ML# "
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1216
  | set_prompts false false = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1217
    ml_prompts ("> " ^ oct_char "372") ("- " ^ oct_char "373");
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1218
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1219
fun init_setup isar pgip =
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1220
 (conditional (not (! initialized)) (fn () =>
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1221
   (if isar then setmp warning_fn (K ()) init_outer_syntax () else ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1222
    setup_xsymbols_output ();
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1223
    setup_pgml_output ();
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1224
    setup_messages ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1225
    setup_state ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1226
    setup_thy_loader ();
13526
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
  1227
    setup_present_hook ();
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1228
    set initialized; ()));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1229
  sync_thy_loader ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1230
  print_mode := proof_generalN :: (! print_mode \ proof_generalN);
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1231
  if pgip then 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1232
      print_mode := pgmlN :: (pgmlatomsN :: (! print_mode \ pgmlN \ pgmlatomsN)) 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1233
    else ();
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1234
  set quick_and_dirty;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1235
  ThmDeps.enable ();
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1236
  set_prompts isar pgip;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1237
  pgip_active := pgip)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1238
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1239
fun init isar = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1240
    (init_setup isar false;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1241
     if isar then ((* da: this welcome is problematic: clashes with welcome
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1242
		      issued for PG anyway. 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1243
		      welcome (); *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1244
		    Isar.sync_main ()) else isa_restart ());
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1245
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1246
fun init_pgip false = panic "Sorry, PGIP not supported for Isabelle/classic mode."
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1247
  | init_pgip true = (init_setup true true; pgip_toplevel tty_src);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1248
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1249
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1250
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1251
(** generate keyword classification elisp file **)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1252
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1253
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1254
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1255
val regexp_meta = explode ".*+?[]^$";
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1256
val regexp_quote = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1257
    implode o map  (fn c => if c mem regexp_meta then "\\\\" ^ c else c)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1258
    o explode;
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1259
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1260
fun defconst name strs =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1261
  "\n(defconst isar-keywords-" ^ name ^
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1262
  "\n  '(" ^ space_implode "\n    " (map (quote o regexp_quote) strs) ^ "))\n";
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1263
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1264
fun make_elisp_commands commands kind =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1265
  defconst kind (mapfilter 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1266
		     (fn (c, _, k, _) => if k = kind then Some c else None) 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1267
		     commands);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1268
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1269
fun make_elisp_syntax (keywords, commands) =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1270
  ";;\n\
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1271
  \;; Keyword classification tables for Isabelle/Isar.\n\
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1272
  \;; This file was generated by " ^ Session.name () ^ " -- DO NOT EDIT!\n\
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1273
  \;;\n\
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1274
  \;; $" ^ "Id$\n\
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1275
  \;;\n" ^
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents: