src/Pure/proof_general.ML
author aspinall
Fri, 03 Sep 2004 00:26:18 +0200
changeset 15173 e1582a0d29b5
parent 15156 daa9f645a26e
child 15191 5ca1fd9dec83
permissions -rw-r--r--
Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
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
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
    10
settings menu in the currently released version of Proof General (3.5).
15134
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
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
    13
The 3.6pre pre-release versions of Emacs Proof General now support the 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
    14
new PGIP format for preferences and restore the settings menu.  
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
    15
Please visit http://proofgeneral.inf.ed.ac.uk/develdownload
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    16
===========================================================================
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    17
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
    18
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
    19
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    20
*)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    21
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    22
signature PROOF_GENERAL =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    23
sig
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    24
  val setup: (theory -> theory) list
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    25
  val update_thy_only: string -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    26
  val try_update_thy_only: string -> unit
13391
553e7b62680f fixed inform_file_retracted: remove_thy;
wenzelm
parents: 13284
diff changeset
    27
  val inform_file_retracted: string -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    28
  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
    29
  val preferences: 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    30
      (string * 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    31
	(string * 
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 * (string * (unit -> string)) * 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    34
	   (string -> unit)))) list) list ref
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
    35
  val process_pgip: string -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    36
  val thms_containing: string list -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    37
  val help: unit -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    38
  val show_context: unit -> theory
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    39
  val kill_goal: unit -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    40
  val repeat_undo: int -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    41
  val isa_restart: unit -> unit
12833
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
    42
  val full_proofs: bool -> unit
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    43
  val isarcmd: string -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    44
  val init: bool -> unit
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    45
  val init_pgip: bool -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    46
  val write_keywords: string -> unit
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
    47
  val xmls_of_str : string -> string list (* temp for testing parser *)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    48
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    49
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    50
structure ProofGeneral : PROOF_GENERAL =
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    51
struct
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    52
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
    53
structure P = OuterParse
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
    54
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    55
(* 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
    56
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    57
val pgip_active = ref false;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    58
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
    59
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    60
fun pgip () = (!pgip_active);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    61
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
    62
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    63
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    64
(* print modes *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    65
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    66
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
    67
val xsymbolsN = Symbol.xsymbolsN;    (* XSymbols symbols *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    68
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
    69
val pgmlatomsN = "PGMLatoms";	     (* variable kind decorations *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    70
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
    71
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    72
fun pgml () = pgmlN mem_string ! print_mode;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    73
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    74
(* text output: print modes for xsymbol and PGML *)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    75
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    76
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    77
14827
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    78
fun xsym_output "\\" = "\\\\"
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    79
  | 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
    80
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    81
fun xsymbols_output s =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    82
  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
    83
    let val syms = Symbol.explode s
14827
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    84
    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
    85
  else Symbol.default_output s;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    86
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    87
fun pgml_sym s =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    88
  (case Symbol.decode s of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    89
    Symbol.Char "\\" => "\\\\"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    90
  | Symbol.Char s => XML.text s
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    91
  | 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
    92
  | 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
    93
  | Symbol.Raw s => s);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    94
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    95
fun pgml_output str =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    96
  let val syms = Symbol.explode str
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    97
  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
    98
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    99
in 
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   100
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   101
fun setup_xsymbols_output () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   102
    Output.add_mode 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   103
	xsymbolsN 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   104
	(xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   105
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   106
fun setup_pgml_output () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   107
    Output.add_mode 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   108
	pgmlN
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   109
	(pgml_output, Symbol.default_indent, Symbol.encode_raw);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   110
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   111
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   112
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
(* token translations *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   115
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   116
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   117
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   118
val end_tag = oct_char "350";
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   119
val class_tag = ("class", oct_char "351");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   120
val tfree_tag = ("tfree", oct_char "352");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   121
val tvar_tag = ("tvar", oct_char "353");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   122
val free_tag = ("free", oct_char "354");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   123
val bound_tag = ("bound", oct_char "355");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   124
val var_tag = ("var", oct_char "356");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   125
val skolem_tag = ("skolem", oct_char "357");
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   126
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   127
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
   128
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   129
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
   130
    (if Output.has_mode pgmlatomsN then 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   131
	 xml_atom kind x
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   132
     else bg_tag ^ x ^ end_tag, 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   133
     real (Symbol.length (Symbol.explode x)));
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   134
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   135
fun free_or_skolem x =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   136
  (case try Syntax.dest_skolem x of
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   137
    None => tagit free_tag x
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   138
  | Some x' => tagit skolem_tag x');
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   139
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   140
fun var_or_skolem s =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   141
  (case Syntax.read_var s of
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   142
    Var ((x, i), _) =>
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   143
      (case try Syntax.dest_skolem x of
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   144
        None => tagit var_tag s
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   145
      | 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
   146
  | _ => tagit var_tag s);
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   147
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   148
val proof_general_trans =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   149
 Syntax.tokentrans_mode proof_generalN
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   150
  [("class", tagit class_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   151
   ("tfree", tagit tfree_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   152
   ("tvar", tagit tvar_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   153
   ("free", free_or_skolem),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   154
   ("bound", tagit bound_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   155
   ("var", var_or_skolem)];
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   156
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   157
in val setup = [Theory.add_tokentrfuns proof_general_trans] end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   158
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   159
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   160
(* assembling PGIP packets *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   161
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   162
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
   163
val pgip_refid = ref None : string option ref
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   164
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   165
local
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   166
    val myseq_no = ref 1;      (* PGIP packet counter *)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   167
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   168
    val pgip_class  = "pg"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   169
    val pgip_origin = "Isabelle/Isar"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   170
    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
   171
		   (Time.toString(Time.now()))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   172
	          (* 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
   173
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   174
    fun assemble_pgips pgips = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   175
	XML.element 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   176
	     "pgip" 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   177
	     ([("class",  pgip_class),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   178
	       ("origin", pgip_origin),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   179
	       ("id",     pgip_id)] @
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   180
	      (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
   181
	      (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
   182
	      [("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
   183
	     pgips
13526
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   184
in
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   185
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   186
 fun decorated_output bg en prfx = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   187
    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
   188
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   189
 (* 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
   190
    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
   191
 fun issue_pgips ps = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   192
     if pgip_emacs_compatibility() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   193
	 decorated_output (* add urgent message annotation *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   194
	     (oct_char "360") (oct_char "361") "" 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   195
	     (assemble_pgips ps)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   196
     else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   197
	 writeln_default (assemble_pgips ps)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   198
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   199
 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
   200
				  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   201
 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
   202
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   203
 (* FIXME: need to add stuff to gather PGIPs here *)
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   204
 fun issue_pgip resp attrs txt = 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   205
     if pgip_emacs_compatibility() then
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   206
	 decorated_output (* add urgent message annotation *)
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   207
	     (oct_char "360") (oct_char "361") "" 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   208
	     (assemble_pgip resp attrs txt)
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   209
     else 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   210
	 writeln_default (assemble_pgip resp attrs txt)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   211
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   212
(*  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
   213
 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
   214
     if pgip_emacs_compatibility() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   215
      (*  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
   216
	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
   217
     else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   218
	issue_pgip resp attrs s
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   219
	
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   220
 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
   221
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   222
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   223
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   224
(* messages and notification *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   225
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   226
local
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   227
    val delay_msgs = ref false   (* whether to accumulate messages *)
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   228
    val delayed_msgs = ref []
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   229
in
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   230
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   231
 fun message resp attrs bg en prfx s =
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   232
     if pgip() then 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   233
	 (if (!delay_msgs) then
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   234
	      delayed_msgs := (resp,attrs,prefix_lines prfx s)::(!delayed_msgs) (* nb: no decs *)
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   235
	  else 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   236
	      issue_pgip_maybe_decorated bg en resp attrs (prefix_lines prfx s))
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   237
     else 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   238
	 decorated_output bg en prfx s;
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   239
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   240
 fun start_delay_msgs () = (delay_msgs := true;
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   241
			    delayed_msgs := [])
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   242
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   243
 fun end_delayed_msgs () = 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   244
     (delay_msgs := false;
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   245
      map (fn (resp,attrs,s) => XML.element resp attrs [s]) (!delayed_msgs))
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   246
end
15134
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
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   249
    val display_area = ("area", "display")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   250
    val message_area = ("area", "message")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   251
    val tracing_category = ("category", "tracing")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   252
    val urgent_indication = ("urgent", "y")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   253
    val nonfatal = ("fatality", "nonfatal")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   254
    val fatal = ("fatality", "fatal")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   255
    val panic = ("fatality", "panic")
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
    val thyname_attr = pair "thyname"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   258
    val url_attr = pair "url"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   259
    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
   260
in			   
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   261
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   262
fun setup_messages () =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   263
 (writeln_fn  := message "normalresponse" [message_area] "" "" "";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   264
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   265
  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
   266
			 (oct_char "360") (oct_char "361") "";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   267
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   268
  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
   269
			(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
   270
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   271
  warning_fn := message "errorresponse"    [nonfatal]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   272
			(oct_char "362") (oct_char "363") "### ";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   273
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   274
  error_fn := message "errorresponse" [fatal]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   275
		      (oct_char "364") (oct_char "365") "*** ";
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   276
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   277
  panic_fn := message "errorresponse" [panic]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   278
		      (oct_char "364") (oct_char "365") "!!! ")
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   279
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
(* 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
   282
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   283
fun with_displaywrap (elt,attrs) dispfn =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   284
    let 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   285
	val lines = ref ([] : string list);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   286
	fun wlgrablines s = (lines:= (s :: (!lines)))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   287
    in 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   288
	(setmp writeln_fn wlgrablines dispfn ();
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   289
	 (* 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
   290
         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
   291
    end
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   292
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   293
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
   294
    
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   295
fun tell_clear_goals () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   296
    if pgip() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   297
	issue_pgipe "cleardisplay" [display_area]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   298
    else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   299
	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
   300
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   301
fun tell_clear_response () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   302
    if pgip() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   303
	issue_pgipe "cleardisplay" [message_area]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   304
    else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   305
	emacs_notify "Proof General, please clear the response buffer.";
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   306
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   307
fun tell_file_loaded path = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   308
    if pgip() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   309
	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
   310
		    [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
   311
		     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
   312
    else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   313
	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
   314
		      ^ quote (File.sysify_path path));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   315
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   316
fun tell_file_retracted path = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   317
    if pgip() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   318
	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
   319
		    [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
   320
		     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
   321
    else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   322
	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
   323
		      ^ quote (File.sysify_path path));
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   324
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   325
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   326
(* theory / proof state output *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   327
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   328
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   329
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   330
    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
   331
			      (oct_char "366", oct_char "367", "") f ()
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   332
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   333
    fun statedisplay prts =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   334
	issue_pgip "proofstate" []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   335
		   (XML.element "pgml" []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   336
				[XML.element "statedisplay" 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   337
					     [] 
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   338
					     [(Pretty.output (Pretty.chunks prts))]])
13545
fcdbd6cf5f9f improved tell_thm_deps;
wenzelm
parents: 13538
diff changeset
   339
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   340
    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
   341
	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
   342
	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
   343
	     
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   344
    fun print_state b st =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   345
	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
   346
	else tmp_markers (fn () => Toplevel.print_state_default b st)
13526
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   347
in
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   348
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   349
 fun setup_state () =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   350
     (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
   351
      Toplevel.print_state_fn := print_state;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   352
      (* 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
   353
      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
   354
				   Toplevel.prompt_state_default));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   355
end
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   356
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   357
end
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   358
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   359
(* misc commands for ProofGeneral/isa *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   360
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   361
fun thms_containing ss =
13284
20c818c966e6 thms_containing: optional limit argument;
wenzelm
parents: 13273
diff changeset
   362
  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
   363
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   364
val welcome = priority o Session.welcome;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   365
val help = welcome;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   366
val show_context = Context.the_context;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   367
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   368
fun kill_goal () = (Goals.reset_goals (); tell_clear_goals ());
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   369
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   370
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
   371
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   372
fun repeat_undo 0 = ()
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   373
  | repeat_undo 1 = undo ()
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   374
  | 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
   375
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   376
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   377
(* theory loader actions *)
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
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   380
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   381
fun add_master_files name files =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   382
  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
   383
  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
   384
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   385
fun trace_action action name =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   386
  if action = ThyInfo.Update then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   387
    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
   388
  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
   389
    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
   390
  else ();
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
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   393
  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
   394
  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
   395
end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   396
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   397
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   398
(* prepare theory context *)
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
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
   401
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
   402
			    false ThyInfo.update_thy_only;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   403
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   404
fun which_context () =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   405
  (case Context.get_context () of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   406
    Some thy => "  Using current (dynamic!) one: " ^
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   407
      (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
   408
  | None => "");
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   409
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   410
fun try_update_thy_only file =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   411
  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
   412
    let val name = thy_name file in
15156
daa9f645a26e Adapted to new interface of function ThyLoad.check_file
berghofe
parents: 15147
diff changeset
   413
      if is_some (ThyLoad.check_file None (ThyLoad.thy_path name)) 
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   414
      then update_thy_only name
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   415
      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
   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
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   419
(* get informed about files *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   420
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   421
val inform_file_retracted = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   422
    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
   423
val inform_file_processed = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   424
    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
   425
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   426
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
   427
  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
   428
    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
   429
     (ThyInfo.touch_child_thys name;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   430
      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
   431
       (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
   432
        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
   433
    else raise Toplevel.UNDEF
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   434
  end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   435
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   436
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
   437
 (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
   438
  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
   439
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   440
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   441
(* restart top-level loop (keeps most state information) *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   442
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   443
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   444
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   445
fun restart isar =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   446
 (if isar then tell_clear_goals () else kill_goal ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   447
  tell_clear_response ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   448
  welcome ());
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   449
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   450
in
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   451
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   452
fun isa_restart () = restart false;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   453
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
   454
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   455
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   456
12833
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   457
fun full_proofs true = proofs := 2
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   458
  | full_proofs false = proofs := 1;
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   459
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   460
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   461
(* theorem dependency output *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   462
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   463
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   464
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   465
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
   466
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   467
fun thm_deps_message (thms, deps) = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   468
    if pgip() then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   469
	issue_pgips 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   470
	    [XML.element
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   471
		 "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
   472
		 [("infotype", "isabelle_theorem_dependencies")]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   473
		 [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
   474
		  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
   475
    else emacs_notify 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   476
	     ("Proof General, theorem dependencies of " 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   477
	      ^ thms ^ " are " ^ deps)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   478
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
fun tell_thm_deps ths =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   481
  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
   482
    let
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   483
      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
   484
      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
   485
				    (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
   486
    in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   487
      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
   488
      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
   489
    end);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   490
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   491
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   492
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   493
fun setup_present_hook () =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   494
  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
   495
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   496
end;
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
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   499
(*** Preferences ***)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   500
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   501
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   502
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
   503
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
   504
					    ("max", string_of_int max)] []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   505
val pgipbool       = XML.element "pgipbool" [] []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   506
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   507
fun withdefault f = (f(), f)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   508
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   509
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   510
fun nat_option r = (pgipnat,
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   511
  withdefault (fn () => string_of_int (!r)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   512
  (fn s => (case Syntax.read_nat s of
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   513
       None => error ("nat_option: illegal value " ^ s)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   514
     | Some i => r := i)));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   515
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   516
fun bool_option r = (pgipbool,
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   517
  withdefault (fn () => Bool.toString (!r)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   518
  (fn "false" => r := false | "true" => r := true
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   519
    | x => error ("bool_option: illegal value" ^ x)));
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   520
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   521
val proof_option = (pgipbool,
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   522
  withdefault (fn () => Bool.toString (!proofs >= 2)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   523
  (fn "false" => proofs := 1 | "true" => proofs := 2
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   524
    | x => error ("proof_option: illegal value" ^ x)));
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   525
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   526
val thm_deps_option = (pgipbool,
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   527
  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
   528
  (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
   529
    | "true" => print_mode := ("thm_deps" ins (!print_mode))
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   530
    | x => error ("thm_deps_option: illegal value " ^ x)));
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   531
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   532
local 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   533
    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
   534
    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
   535
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   536
val print_depth_option = (pgipnat,
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   537
  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
   538
  (fn s => (case Syntax.read_nat s of
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   539
       None => error ("print_depth_option: illegal value" ^ s)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   540
     | Some i => pg_print_depth i)))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   541
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   542
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   543
val preferences = ref 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   544
  [("Display",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   545
    [("show-types", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   546
      ("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
   547
       bool_option show_types)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   548
     ("show-sorts", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   549
      ("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
   550
       bool_option show_sorts)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   551
     ("show-consts", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   552
      ("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
   553
       bool_option show_consts)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   554
     ("long-names", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   555
      ("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
   556
     ("show-brackets", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   557
      ("Show full bracketing in Isabelle terms",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   558
       bool_option show_brackets)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   559
     ("show-main-goal", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   560
      ("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
   561
     ("eta-contract", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   562
      ("Print terms eta-contracted",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   563
       bool_option Syntax.eta_contract))]),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   564
   ("Advanced Display",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   565
    [("goals-limit", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   566
      ("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
   567
       nat_option goals_limit)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   568
     ("prems-limit", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   569
      ("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
   570
       nat_option ProofContext.prems_limit)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   571
     ("print-depth", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   572
      ("Setting for the ML print depth",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   573
       print_depth_option))]),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   574
   ("Tracing",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   575
    [("trace-simplifier", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   576
      ("Trace simplification rules.",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   577
       bool_option trace_simp)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   578
     ("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
   579
		      bool_option trace_rules)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   580
     ("trace-unification", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   581
      ("Output error diagnostics during unification",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   582
       bool_option Pattern.trace_unify_fail)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   583
     ("global-timing", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   584
      ("Whether to enable timing in Isabelle.",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   585
       bool_option Output.timing))]),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   586
   ("Proof", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   587
    [("quick-and-dirty", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   588
      ("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
   589
       bool_option quick_and_dirty)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   590
     ("full-proofs", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   591
      ("Record full proof objects internally",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   592
       proof_option)),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   593
     ("theorem-dependencies", 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   594
       ("Track theorem dependencies within Proof General",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   595
	thm_deps_option))])
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   596
   ];
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   597
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   598
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   599
(* Configuration: GUI config, proverinfo messages *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   600
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   601
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   602
    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
   603
    val name_attr = pair "name"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   604
    val version_attr = pair "version"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   605
    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
   606
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   607
fun send_pgip_config () =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   608
    let 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   609
	val path = Path.unpack config_file
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   610
	val exists = File.exists path
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   611
	val proverinfo = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   612
	    XML.element "proverinfo"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   613
              [("name",Session.name()), ("version", version),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   614
	       ("url", isabelle_www)]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   615
	    [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
   616
	     XML.element "helpdoc" 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   617
         (* 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
   618
          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
   619
          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
   620
		      [("name", "Isabelle/HOL Tutorial"),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   621
		       ("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
   622
		       ("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
   623
	      []]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   624
    in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   625
	if exists then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   626
	    (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
   627
	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
   628
    end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   629
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   630
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   631
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   632
(* PGIP identifier tables (prover objects). [incomplete] *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   633
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   634
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   635
    val objtype_thy  = "theory"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   636
    val objtype_thm  = "theorem"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   637
    val objtype_term = "term"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   638
    val objtype_type = "type"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   639
		       
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   640
    fun xml_idtable ty ctx ids = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   641
	let
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   642
            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
   643
              | ctx_attr None    = []
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   644
	    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
   645
	in 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   646
	    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
   647
	                          (map xmlid ids)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   648
	end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   649
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   650
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   651
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
   652
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
   653
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
   654
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   655
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
   656
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   657
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
   658
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
   659
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   660
fun send_thm_idtable ctx thy = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   661
    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
   662
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   663
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
   664
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   665
(* 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
   666
   & maybe not so useful anyway *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   667
	
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   668
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   669
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   670
(* 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
   671
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   672
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   673
 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
   674
 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
   675
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   676
 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
   677
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   678
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
   679
  | 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
   680
                           (* only theories known in top context *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   681
  | 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
   682
  | 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
   683
  | 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
   684
                               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
   685
  | 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
   686
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   687
fun showid (_,        "theory", n) = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   688
    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
   689
  | showid (Some thy, "theorem", t) = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   690
    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
   691
  | showid (None,     "theorem", t) = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   692
    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
   693
  | 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
   694
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   695
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   696
	 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   697
(** Parsing proof scripts without execution **)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   698
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   699
(* Notes.
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   700
   This is quite tricky, because 1) we need to put back whitespace which
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   701
   was removed during parsing so we can provide markup around commands;
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   702
   2) parsing is intertwined with execution in Isar so we have to repeat
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   703
   the parsing to extract interesting parts of commands.  The trace of
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   704
   tokens parsed which is now recorded in each transition helps do this.
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   705
   
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   706
   If we had proper parse trees it would be easy, or if we could go
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   707
   beyond ML's type system to allow existential types to be part of
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   708
   parsers (the quantified type representing the result of the parse
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   709
   which is used to make the transition function) it might be possible.
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   710
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   711
   Probably the best solution is to produce the meta-information at
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   712
   the same time as the parse, for each command, e.g. by recording a 
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   713
   list of (name,objtype) pairs which record the bindings created by 
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   714
   a command.  This would require changing the interfaces in 
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   715
   outer_syntax.ML (or providing new ones), 
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   716
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   717
    datatype metainfo = Binding of string * string  (* name, objtype *)
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   718
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   719
    val command_withmetainfo: string -> string -> string ->
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   720
      (token list -> 
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   721
       ((Toplevel.transition -> Toplevel.transition) * metainfo list) * 
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   722
       token list) -> parser
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   723
*)
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   724
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   725
local
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   726
    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
   727
    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
   728
    fun empty elt = [XML.element elt [] []]
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   729
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   730
    (* an extra token is needed to terminate the command *)
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   731
    val sync = OuterSyntax.scan "\\<^sync>";
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   732
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   733
    fun named_item_elt_with nameattr toks str elt nameP objtyp = 
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   734
	let 
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   735
	    val name = (fst (nameP (toks@sync)))
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   736
			handle _ => (error ("Error occurred in name parser for " ^ elt ^ 
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   737
					    "(objtype: " ^ objtyp ^ ")");
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   738
				     "")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   739
				     
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   740
	in 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   741
	    [XML.element elt 
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   742
			 ((if name="" then [] else [(nameattr, name)])@
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   743
			  (if objtyp="" then [] else [("objtype", objtyp)]))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   744
			 ([XML.text str])]
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   745
	end
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   746
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   747
    val named_item_elt = named_item_elt_with "name"
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   748
    val thmnamed_item_elt = named_item_elt_with "thmname"
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   749
 
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   750
    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
   751
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   752
    (* 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
   753
       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
   754
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   755
    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
   756
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   757
    fun get_keywords_classification_table () = 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   758
	case (!keywords_classification_table) of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   759
	    Some t => t
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   760
	  | None => (let
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   761
			 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
   762
					 (Symtab.empty,OuterSyntax.dest_parsers())
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   763
		     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
   764
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   765
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   766
		    
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   767
    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
   768
	let 
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   769
	    val ((thyname,imports,files),_) = ThyHeader.args (toks@sync)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   770
	in 
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   771
	    markup_text_attrs str "opentheory" [("thyname",thyname),
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   772
						("parentnames", space_implode ";" imports)]
15145
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_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
   776
	let 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   777
	    (* 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
   778
	       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
   779
	       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
   780
	       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
   781
	       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
   782
	       instead of reconstructing it here. *)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   783
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   784
	    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
   785
		["defaultsort","arities","judgement","finalconsts",
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   786
		 "syntax", "nonterminals", "translations",
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   787
		 "global", "local", "hide",
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   788
		 "ML_setup", "setup", "method_setup",
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   789
		 "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
   790
		 "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
   791
		 "oracle",
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   792
		 "declare"]
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   793
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   794
	    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
   795
	    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
   796
	    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
   797
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   798
	    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
   799
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   800
	    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
   801
		let 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   802
		    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
   803
		    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
   804
		in 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   805
		    theoremsP
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   806
		end
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   807
	in 
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   808
	    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
   809
	    else case name of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   810
		     "text"      => comment_item
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   811
		   | "text_raw"  => comment_item
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   812
		   | "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
   813
		   | "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
   814
		   | "classes"   => named_item P.name "class"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   815
		   | "classrel"  => named_item P.name "class"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   816
		   | "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
   817
		   | "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
   818
		   | "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
   819
		   | "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
   820
		   | "theorems"  => named_item thmnameP "thmset"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   821
		   | "lemmas"    => named_item thmnameP "thmset"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   822
		   | "oracle"    => named_item P.name "oracle"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   823
		   | "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
   824
		   | _ => (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
   825
	end
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_thy_goal (name,toks,str) = 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   828
	let 
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   829
	    (* see isar_syn.ML/gen_theorem *)
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   830
         val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp);
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   831
	 val general_statement =
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   832
	    statement >> pair [] || Scan.repeat P.locale_elem_or_expr -- (P.$$$ "shows" |-- statement);
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   833
	    
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   834
	    val gen_theoremP =
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   835
		P.locale_target -- Scan.optional (P.opt_thm_name ":" --|
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   836
                 Scan.ahead (P.locale_keyword || P.$$$ "shows")) ("", []) --
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   837
				 general_statement >> (fn ((locale, a), (elems, concl)) => 
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   838
							 fst a) (* a : (bstring * Args.src list) *)
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   839
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   840
	    val nameP = P.locale_target |-- (Scan.optional ((P.opt_thm_name ":") >> #1) "")
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   841
	    (* TODO: add preference values for attributes 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   842
	       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
   843
	    *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   844
	in 
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   845
	    thmnamed_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
   846
	end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   847
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   848
    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
   849
      "sorry"         => markup "giveupgoal"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   850
    | "oops"          => markup "postponegoal"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   851
    | "done"          => markup "closegoal" 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   852
    | "by"            => markup "closegoal"  (* nested or toplevel *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   853
    | "qed"           => markup "closegoal"  (* nested or toplevel *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   854
    | "."	      => markup "closegoal"  (* nested or toplevel *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   855
    | ".."	      => markup "closegoal"  (* nested or toplevel *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   856
    | 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
   857
      (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
   858
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   859
    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
   860
    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
   861
    case kind of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   862
      "control"        => markup "badcmd"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   863
    | "diag"           => markup "spuriouscmd"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   864
    (* theory/files *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   865
    | "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
   866
    | "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
   867
    | "theory-heading" => markup "litcomment"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   868
    | "theory-script"  => markup "theorystep"
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   869
    | "theory-end"     => markup "closetheory"
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   870
    (* proof control *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   871
    | "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
   872
    | "proof-heading"  => markup "litcomment"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   873
    | "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
   874
    | "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
   875
    | "proof-open"     => (empty "openblock") @ (markup "proofstep")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   876
    | "proof-close"    => (markup "proofstep") @ (empty "closeblock")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   877
    | "proof-script"   => markup "proofstep"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   878
    | "proof-chain"    => markup "proofstep"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   879
    | "proof-decl"     => markup "proofstep"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   880
    | "proof-asm"      => markup "proofstep"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   881
    | "proof-asm-goal" => markup "proofstep"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   882
    | "qed"            => xmls_of_qed (name,markup)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   883
    | "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
   884
    | "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
   885
    | 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
   886
      (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
   887
       markup "spuriouscmd")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   888
    end 
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   889
in
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   890
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   891
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
   892
   let 
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   893
       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
   894
   in case classification of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   895
	  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
   896
	| 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
   897
	  (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
   898
	   markup_text str "spuriouscmd")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   899
   end 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   900
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   901
fun xmls_of_impropers [] = []
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   902
  | xmls_of_impropers toks = 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   903
    let 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   904
	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
   905
	fun markup [] _ = []
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   906
	  | 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
   907
    in
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   908
	(markup whs "comment") @ (markup rest "unparseable")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   909
    end
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   910
    
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   911
fun markup_unparseable str = markup_text str "unparseable" 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   912
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   913
end
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   914
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   915
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   916
local
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   917
    (* 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
   918
       to reconstruct the input. *)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   919
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   920
    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
   921
      | 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
   922
	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
   923
	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
   924
      | 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
   925
in
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   926
    fun xmls_of_str str =
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   927
    let 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   928
       (* 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
   929
       fun parse_loop ([],[],xmls) = xmls
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   930
	 | 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
   931
	 | 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
   932
	   let 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   933
	       (* 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
   934
	       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
   935
	       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
   936
						  | _ => error("proof_general/parse_loop impossible") 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   937
	       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
   938
               (* 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
   939
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   940
	       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
   941
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   942
	       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
   943
	       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
   944
	   in
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   945
	       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
   946
	   end
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   947
    in
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   948
	(let val toks = OuterSyntax.scan str
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   949
	 in 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   950
	     parse_loop (OuterSyntax.read toks, toks, [])
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   951
	 end)
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   952
 	   handle _ => markup_unparseable str
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   953
    end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   954
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   955
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   956
fun parsescript str attrs = 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   957
    let 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   958
	val _ = start_delay_msgs ()  (* accumulate error messages to put inside parseresult *)
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   959
	val xmls = xmls_of_str str
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   960
        val errs = end_delayed_msgs ()
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   961
     in 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   962
	issue_pgips [XML.element "parseresult" attrs (errs@xmls)]
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
   963
    end
15134
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
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   968
(**** PGIP:  Isabelle -> Interface ****)
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
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
   971
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
   972
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   973
fun usespgip () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   974
    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
   975
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   976
fun usespgml () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   977
    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
   978
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   979
fun hasprefs () = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   980
    seq (fn (prefcat, prefs) =>
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   981
	    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
   982
		 (map (fn (name, (descr, (ty, (default,_),_))) => 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   983
		       XML.element "haspref" [("name", name), 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   984
					      ("descr", descr), 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   985
					      ("default", default)]
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   986
		       [ty]) prefs)]) (!preferences);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   987
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   988
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
   989
	
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   990
fun setpref name value = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   991
    (case assoc (allprefs(), name) of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   992
	 None => warning ("Unknown pref: " ^ quote name)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   993
       | Some (_, (_, _, set)) => set value);
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   994
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   995
fun getpref name = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   996
    (case assoc (allprefs(), name) of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   997
	 None => warning ("Unknown pref: " ^ quote name)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   998
       | Some (_, (_, (_,get), _)) => 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   999
	   issue_pgip "prefval" [("name", name)] (get ()));
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1000
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1001
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1002
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1003
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1004
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1005
(**** PGIP:  Interface -> Isabelle/Isar ****)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1006
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1007
exception PGIP of string;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1008
exception PGIP_QUIT;
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
(* Sending commands to Isar *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1011
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1012
fun isarcmd s = 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1013
    s |> OuterSyntax.scan |> OuterSyntax.read 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1014
      |> 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
  1015
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1016
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
  1017
  | xmltext [] = ""
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1018
  | 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
  1019
			
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1020
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
  1021
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1022
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1023
(* 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
  1024
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1025
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
  1026
    let
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1027
	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
  1028
    in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1029
	case extn of
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1030
	    "" => 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
  1031
	  | "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
  1032
	  | "ML" => isarcmd ("use " ^ quote file)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1033
	  (* 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
  1034
	  | 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
  1035
    end  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1036
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1037
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1038
(* Proof control commands *)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1039
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1040
local
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1041
  fun xmlattro attr attrs = assoc(attrs,attr)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1042
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1043
  fun xmlattr attr attrs = 
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1044
      (case xmlattro attr attrs of 
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1045
	   Some value => value 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1046
	 | None => raise PGIP ("Missing attribute: " ^ attr))
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1047
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1048
  val thyname_attro = xmlattro "thyname"
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1049
  val thyname_attr = xmlattr "thyname"
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1050
  val objtype_attro = xmlattro "objtype"
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1051
  val objtype_attr = xmlattr "objtype"
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1052
  val name_attr = xmlattr "name"
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1053
  val dirname_attr = xmlattr "dir"
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1054
  fun comment x = "(* " ^ x ^ " *)"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1055
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1056
  fun localfile_of_url url = (* only handle file:/// or file://localhost/ *)
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1057
      case Url.unpack url of
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1058
	  (Url.File path) => File.sysify_path path
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1059
	| _ => error ("Cannot access non-local URL " ^ url)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1060
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1061
  val fileurl_of = localfile_of_url o (xmlattr "url")
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1062
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1063
  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
  1064
  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
  1065
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1066
  val currently_open_file = ref (None : string option)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1067
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1068
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1069
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
  1070
  (XML.Text t) => warning ("Ignored text in PGIP packet: \n" ^ t)
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1071
| (xml as (XML.Elem (elem, attrs, data))) => 
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1072
  (case elem of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1073
       (* protocol config *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1074
       "askpgip"  	=> (usespgip (); send_pgip_config ())
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1075
     | "askpgml"  	=> usespgml ()
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1076
     (* proverconfig *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1077
     | "askprefs" 	=> hasprefs ()
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1078
     | "getpref"  	=> getpref (name_attr attrs)
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1079
     | "setpref"  	=> setpref (name_attr attrs) (xmltext data)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1080
     (* provercontrol *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1081
     | "proverinit" 	=> isar_restart ()
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1082
     | "proverexit" 	=> isarcmd "quit"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1083
     | "startquiet" 	=> isarcmd "disable_pr"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1084
     | "stopquiet"  	=> isarcmd "enable_pr"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1085
     | "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
  1086
     | "pgmlsymbolsoff"  => (print_mode := (Library.gen_rems 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1087
						(op =) 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1088
						(! print_mode, ["xsymbols", "symbols"])))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1089
     (* 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
  1090
     | "opengoal"       => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1091
     | "proofstep"      => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1092
     | "closegoal"      => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1093
     | "giveupgoal"     => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1094
     | "postponegoal"   => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1095
     | "comment"	=> isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1096
     | "litcomment"     => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1097
     | "spuriouscmd"    => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1098
     | "badcmd"		=> isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1099
     (* 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
  1100
     | "undostep"       => isarcmd "ProofGeneral.undo"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1101
     | "abortgoal"      => isarcmd "ProofGeneral.kill_proof"  
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1102
     | "forget"         => error "Not implemented" 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1103
     | "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
  1104
     (* proofctxt: improper commands *)
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1105
     | "askids"         => askids (thyname_attro attrs, objtype_attro attrs)
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1106
     | "showid"	        => showid (thyname_attro attrs, objtype_attr attrs, name_attr attrs)
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1107
     | "parsescript"    => parsescript (xmltext data) attrs (* just pass back attrs unchanged *)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1108
     | "showproofstate" => isarcmd "pr"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1109
     | "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
  1110
     | "searchtheorems" => isarcmd ("thms_containing " ^ (xmltext data))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1111
     | "setlinewidth"   => isarcmd ("pretty_setmargin " ^ (xmltext data))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1112
     | "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
  1113
     (* properfilecmd: proper theory-level script commands *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1114
     | "opentheory"     => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1115
     | "theoryitem"     => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1116
     | "closetheory"    => (isarscript data;
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1117
			    writeln ("Theory "^(topthy_name())^" completed."))
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1118
     (* 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
  1119
     | "aborttheory"    => isarcmd ("init_toplevel")
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1120
     | "retracttheory"  => isarcmd ("kill_thy " ^ (quote (thyname_attr attrs)))
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1121
     | "loadfile"       => use_thy_or_ml_file (fileurl_of attrs)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1122
     | "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
  1123
			    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
  1124
     | "closefile"      => (case !currently_open_file of 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1125
				Some f => (inform_file_processed f;
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1126
					   currently_open_file := None)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1127
			      | 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
  1128
     | "abortfile"      => (currently_open_file := None) (* perhaps error for no file open *)
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1129
     | "changecwd"      => ThyLoad.add_path (dirname_attr attrs)
15147
e1ed51e0ec0f Add systemcmd.
aspinall
parents: 15146
diff changeset
  1130
     | "systemcmd"	=> isarscript data
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1131
     (* unofficial command for debugging *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1132
     | "quitpgip" => raise PGIP_QUIT  
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1133
     | _ => 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
  1134
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1135
fun process_pgip_tree xml = 
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1136
    (pgip_refseq := None; 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1137
     pgip_refid := None;
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1138
     (case xml of
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1139
	  XML.Elem ("pgip", attrs, pgips) => 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1140
	  (let 
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1141
	       val class = xmlattr "class" attrs
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1142
	       val _ = (pgip_refseq := xmlattro "seq" attrs;
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1143
			pgip_refid :=  xmlattro "id" attrs)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1144
	   in  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1145
	       if (class = "pa") then
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1146
		   seq process_pgip_element pgips
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1147
	       else 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1148
		   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
  1149
	   end)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1150
	| _ => raise PGIP "Invalid PGIP packet received") 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1151
     handle (PGIP msg) => 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1152
	    (error (msg ^ "\nPGIP error occured in XML text below:\n" ^ 
15173
e1582a0d29b5 Comment about 3.6pre. Clean ups to XML, URL handling. Fix statedisplay double PGML quoting. Accumulate parse errors inside parseresult.
aspinall
parents: 15156
diff changeset
  1153
		    (XML.string_of_tree xml))))
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1154
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1155
(* for export to Emacs *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1156
(* 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
  1157
(* 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
  1158
   during output *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1159
fun process_pgip s = 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1160
    (pgip_emacs_compatibility_flag := true;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1161
     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
  1162
     pgip_emacs_compatibility_flag := false)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1163
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1164
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1165
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1166
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1167
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1168
(* PGIP loop: process PGIP input only *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1169
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1170
local  
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1171
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1172
exception XML_PARSE
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1173
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1174
fun loop src : unit =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1175
    let 
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1176
	val _ = issue_pgipe "ready" []
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1177
	val pgipo = (Source.get_single src) 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1178
			handle e => raise XML_PARSE
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1179
    in
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1180
	case pgipo of  
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1181
	     None  => ()
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1182
	   | Some (pgip,src') =>  
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1183
	     ((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
  1184
    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
  1185
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1186
and handler (e,srco) = 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1187
    case (e,srco) of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1188
        (XML_PARSE,Some src) => 
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1189
	(* (!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
  1190
         panic "Invalid XML input, aborting"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1191
      | (PGIP_QUIT,_) => ()
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1192
      | (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
  1193
      | (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
  1194
      | (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
  1195
      | (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
  1196
      | (_,None) => ()
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1197
in
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1198
  (* 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
  1199
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1200
  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
  1201
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1202
  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
  1203
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1204
  val pgip_toplevel =  loop 
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1205
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1206
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1207
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1208
(* additional outer syntax for Isar *)
12778
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
local structure P = OuterParse and K = OuterSyntax.Keyword in
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1211
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1212
val undoP = (* undo without output *)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1213
  OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1214
    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1215
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1216
val context_thy_onlyP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1217
  OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1218
    (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
  1219
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1220
val try_context_thy_onlyP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1221
  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
  1222
    (P.name >> (Toplevel.no_timing oo
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1223
      (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
  1224
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1225
val restartP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1226
  OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1227
    (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
  1228
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1229
val kill_proofP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1230
  OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1231
    (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
  1232
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1233
val inform_file_processedP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1234
  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
  1235
    (P.name >> (fn file => Toplevel.no_timing o
bef0dc694c48 Path.split_ext; more robust inform_file_processed;
wenzelm
parents: 14880
diff changeset
  1236
      Toplevel.keep (vacuous_inform_file_processed file) o
bef0dc694c48 Path.split_ext; more robust inform_file_processed;
wenzelm
parents: 14880
diff changeset
  1237
      Toplevel.kill o
bef0dc694c48 Path.split_ext; more robust inform_file_processed;
wenzelm
parents: 14880
diff changeset
  1238
      Toplevel.keep (proper_inform_file_processed file)));
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1239
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1240
val inform_file_retractedP =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1241
  OuterSyntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" K.control
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1242
    (P.name >> (Toplevel.no_timing oo
14902
bef0dc694c48 Path.split_ext; more robust inform_file_processed;
wenzelm
parents: 14880
diff changeset
  1243
      (fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1244
14725
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
  1245
val process_pgipP =
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
  1246
  OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
  1247
    (P.text >> (Toplevel.no_timing oo
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
  1248
      (fn txt => Toplevel.imperative (fn () => process_pgip txt))));
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
  1249
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1250
fun init_outer_syntax () = OuterSyntax.add_parsers
14675
08b9c690f9cf removed obsolete 'undo';
wenzelm
parents: 14568
diff changeset
  1251
 [undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
14725
2ed5b960c6b1 ProofGeneral.process_pgip command;
wenzelm
parents: 14707
diff changeset
  1252
  inform_file_processedP, inform_file_retractedP, process_pgipP];
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1253
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1254
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1255
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1256
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1257
(* init *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1258
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1259
val initialized = ref false;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
  1260