src/Pure/proof_general.ML
author wenzelm
Sat, 21 Jan 2006 23:02:14 +0100
changeset 18728 6790126ab5f6
parent 18708 4b3dadb4fe33
child 18993 f055b4fe381e
permissions -rw-r--r--
simplified type attribute;
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
17469
4524bf3026d3 tuned comments;
wenzelm
parents: 17417
diff changeset
     5
Isabelle configuration for Proof General (see
4524bf3026d3 tuned comments;
wenzelm
parents: 17417
diff changeset
     6
http://proofgeneral.inf.ed.ac.uk).  Also includes experimental support
4524bf3026d3 tuned comments;
wenzelm
parents: 17417
diff changeset
     7
for PGIP control language for Isabelle/Isar (PGIP 2.X).
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
     8
*)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
     9
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    10
signature PROOF_GENERAL =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    11
sig
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    12
  val update_thy_only: string -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    13
  val try_update_thy_only: string -> unit
13391
553e7b62680f fixed inform_file_retracted: remove_thy;
wenzelm
parents: 13284
diff changeset
    14
  val inform_file_retracted: string -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    15
  val inform_file_processed: string -> unit
16534
wenzelm
parents: 16486
diff changeset
    16
  val preferences:
wenzelm
parents: 16486
diff changeset
    17
      (string *
wenzelm
parents: 16486
diff changeset
    18
        (string *
wenzelm
parents: 16486
diff changeset
    19
         (string *
wenzelm
parents: 16486
diff changeset
    20
          (string * (string * (unit -> string)) *
wenzelm
parents: 16486
diff changeset
    21
           (string -> unit)))) list) list ref
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
    22
  val process_pgip: string -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    23
  val thms_containing: string list -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    24
  val help: unit -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    25
  val show_context: unit -> theory
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    26
  val kill_goal: unit -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    27
  val repeat_undo: int -> unit
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    28
  val isa_restart: unit -> unit
12833
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
    29
  val full_proofs: bool -> unit
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    30
  val isarcmd: string -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    31
  val init: bool -> unit
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    32
  val init_pgip: bool -> unit
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    33
  val write_keywords: string -> unit
16534
wenzelm
parents: 16486
diff changeset
    34
  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
    35
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    36
16534
wenzelm
parents: 16486
diff changeset
    37
structure ProofGeneral: PROOF_GENERAL =
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    38
struct
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    39
16534
wenzelm
parents: 16486
diff changeset
    40
structure P = OuterParse;
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
    41
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
    42
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    43
(* 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
    44
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    45
val pgip_active = ref false;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    46
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
    47
16534
wenzelm
parents: 16486
diff changeset
    48
fun pgip () = (! pgip_active);
wenzelm
parents: 16486
diff changeset
    49
fun pgip_emacs_compatibility () = (! pgip_emacs_compatibility_flag);
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    50
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    51
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    52
(* print modes *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    53
16534
wenzelm
parents: 16486
diff changeset
    54
val proof_generalN = "ProofGeneral";  (*token markup (colouring vars, etc.)*)
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
    55
val pgasciiN = "PGASCII";             (*plain 7-bit ASCII communication*)
16534
wenzelm
parents: 16486
diff changeset
    56
val xsymbolsN = Symbol.xsymbolsN;     (*X-Symbol symbols*)
wenzelm
parents: 16486
diff changeset
    57
val pgmlN = "PGML";                   (*XML escapes and PGML symbol elements*)
wenzelm
parents: 16486
diff changeset
    58
val pgmlatomsN = "PGMLatoms";         (*variable kind decorations*)
wenzelm
parents: 16486
diff changeset
    59
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
    60
16534
wenzelm
parents: 16486
diff changeset
    61
fun pgml () = Output.has_mode pgmlN;
wenzelm
parents: 16486
diff changeset
    62
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
    63
fun special oct =
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
    64
  if Output.has_mode pgasciiN then chr 1 ^ chr (ord (oct_char oct) - 167)
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
    65
  else oct_char oct;
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
    66
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    67
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    68
(* text output: print modes for xsymbol and PGML *)
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    69
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    70
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    71
14827
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    72
fun xsym_output "\\" = "\\\\"
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    73
  | 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
    74
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    75
fun xsymbols_output s =
16534
wenzelm
parents: 16486
diff changeset
    76
  if Output.has_mode xsymbolsN andalso exists_string (equal "\\") s then
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    77
    let val syms = Symbol.explode s
14827
d973e7f820cb Output.add_mode; Output.timing;
wenzelm
parents: 14725
diff changeset
    78
    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
    79
  else Symbol.default_output s;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    80
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    81
fun pgml_sym s =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    82
  (case Symbol.decode s of
16534
wenzelm
parents: 16486
diff changeset
    83
    (*NB: an alternative here would be to output the default print mode alternative
wenzelm
parents: 16486
diff changeset
    84
      in the element content, but unfortunately print modes are not that fine grained.*)
15266
0398af5501fe Revert change to pgml_sym
aspinall
parents: 15254
diff changeset
    85
    Symbol.Char s => XML.text s
15403
9e58e666074d Fix pgmlsymbolson/off.
aspinall
parents: 15401
diff changeset
    86
  | Symbol.Sym sn => XML.element "sym" [("name", sn)] [XML.text s]
16534
wenzelm
parents: 16486
diff changeset
    87
  | Symbol.Ctrl sn => XML.element "ctrl" [("name", sn)] [XML.text s] (* FIXME: no such PGML! *)
15266
0398af5501fe Revert change to pgml_sym
aspinall
parents: 15254
diff changeset
    88
  | Symbol.Raw s => s);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    89
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    90
fun pgml_output str =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    91
  let val syms = Symbol.explode str
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
    92
  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
    93
16534
wenzelm
parents: 16486
diff changeset
    94
in
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    95
16534
wenzelm
parents: 16486
diff changeset
    96
fun setup_xsymbols_output () =
wenzelm
parents: 16486
diff changeset
    97
  Output.add_mode xsymbolsN
wenzelm
parents: 16486
diff changeset
    98
    (xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
    99
16534
wenzelm
parents: 16486
diff changeset
   100
fun setup_pgml_output () =
wenzelm
parents: 16486
diff changeset
   101
  Output.add_mode pgmlN
wenzelm
parents: 16486
diff changeset
   102
    (pgml_output, Symbol.default_indent, Symbol.encode_raw);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   103
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   104
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   105
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   106
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   107
(* token translations *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   108
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   109
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   110
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   111
fun end_tag () = special "350";
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   112
val class_tag = ("class", fn () => special "351");
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   113
val tfree_tag = ("tfree", fn () => special "352");
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   114
val tvar_tag = ("tvar", fn () => special "353");
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   115
val free_tag = ("free", fn () => special "354");
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   116
val bound_tag = ("bound", fn () => special "355");
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   117
val var_tag = ("var", fn () => special "356");
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   118
val skolem_tag = ("skolem", fn () => special "357");
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   119
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   120
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
   121
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   122
fun tagit (kind, bg_tag) x =
16534
wenzelm
parents: 16486
diff changeset
   123
 (if Output.has_mode pgmlatomsN then xml_atom kind x
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   124
  else bg_tag () ^ x ^ end_tag (), real (Symbol.length (Symbol.explode x)));
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   125
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   126
fun free_or_skolem x =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   127
  (case try Syntax.dest_skolem x of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   128
    NONE => tagit free_tag x
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   129
  | SOME x' => tagit skolem_tag x');
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   130
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   131
fun var_or_skolem s =
15985
f00dd5e06ffe renamed show_var_qmarks to show_question_marks;
wenzelm
parents: 15964
diff changeset
   132
  (case Syntax.read_variable s of
f00dd5e06ffe renamed show_var_qmarks to show_question_marks;
wenzelm
parents: 15964
diff changeset
   133
    SOME (x, i) =>
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   134
      (case try Syntax.dest_skolem x of
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   135
        NONE => tagit var_tag s
15992
cb02d70a2040 var_or_skolem: always print question mark for vars stemming from skolems;
wenzelm
parents: 15985
diff changeset
   136
      | SOME x' => tagit skolem_tag
cb02d70a2040 var_or_skolem: always print question mark for vars stemming from skolems;
wenzelm
parents: 15985
diff changeset
   137
          (setmp show_question_marks true Syntax.string_of_vname (x', i)))
15985
f00dd5e06ffe renamed show_var_qmarks to show_question_marks;
wenzelm
parents: 15964
diff changeset
   138
  | NONE => tagit var_tag s);
12778
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
val proof_general_trans =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   141
 Syntax.tokentrans_mode proof_generalN
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   142
  [("class", tagit class_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   143
   ("tfree", tagit tfree_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   144
   ("tvar", tagit tvar_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   145
   ("free", free_or_skolem),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   146
   ("bound", tagit bound_tag),
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   147
   ("var", var_or_skolem)];
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   148
15801
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15629
diff changeset
   149
in
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15629
diff changeset
   150
18708
4b3dadb4fe33 setup: theory -> theory;
wenzelm
parents: 18678
diff changeset
   151
val _ = Context.add_setup (Theory.add_tokentrfuns proof_general_trans);
15801
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15629
diff changeset
   152
d2f5ca3c048d superceded by Pure.thy and CPure.thy;
wenzelm
parents: 15629
diff changeset
   153
end;
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   154
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   155
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   156
(* assembling PGIP packets *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   157
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   158
val pgip_refid  = ref NONE: string option ref;
16534
wenzelm
parents: 16486
diff changeset
   159
val pgip_refseq = ref NONE: string option ref;
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   160
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   161
local
16821
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   162
  val pgip_class  = "pg"
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   163
  val pgip_tag = "Isabelle/Isar"
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   164
  val pgip_id = ref ""
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   165
  val pgip_seq = ref 0
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   166
  fun pgip_serial () = inc pgip_seq
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   167
16534
wenzelm
parents: 16486
diff changeset
   168
  fun assemble_pgips pgips =
wenzelm
parents: 16486
diff changeset
   169
    XML.element
wenzelm
parents: 16486
diff changeset
   170
      "pgip"
16821
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   171
      ([("tag",    pgip_tag),
17407
38e0219ec022 Revert previous attribute name change, problem can be avoided in JAXB.
aspinall
parents: 17403
diff changeset
   172
        ("class",  pgip_class),
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   173
        ("seq",    string_of_int (pgip_serial())),
16821
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   174
        ("id",     !pgip_id)] @
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   175
       if_none (Option.map (single o (pair "destid")) (! pgip_refid)) [] @
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   176
       (* destid=refid since Isabelle only communicates back to sender,
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   177
          so we may omit refid from attributes.
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   178
       if_none (Option.map (single o (pair "refid"))  (! pgip_refid)) [] @
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   179
       *)
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   180
       if_none (Option.map (single o (pair "refseq")) (! pgip_refseq)) [])
16534
wenzelm
parents: 16486
diff changeset
   181
      pgips;
16821
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   182
13526
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   183
in
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   184
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   185
fun init_pgip_session_id () =
16821
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   186
    pgip_id := getenv "HOSTNAME" ^ "/" ^ getenv "USER" ^ "/" ^
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   187
               getenv "ISABELLE_PID" ^ "/" ^ Time.toString (Time.now ())
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   188
16821
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   189
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   190
fun matching_pgip_id id = (id = !pgip_id)
ba1f6aba44ed Update PGIP packet handling, fixing unique session identifier.
aspinall
parents: 16816
diff changeset
   191
16534
wenzelm
parents: 16486
diff changeset
   192
fun decorated_output bg en prfx =
wenzelm
parents: 16486
diff changeset
   193
  writeln_default o enclose bg en o prefix_lines prfx;
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   194
16534
wenzelm
parents: 16486
diff changeset
   195
(* FIXME: see Rev 1.48 [PG CVS] for cleaner version of this which can be used
wenzelm
parents: 16486
diff changeset
   196
   for PG 4.0 which processes PGIP without needing special chars *)
wenzelm
parents: 16486
diff changeset
   197
fun issue_pgips ps =
wenzelm
parents: 16486
diff changeset
   198
  if pgip_emacs_compatibility() then
wenzelm
parents: 16486
diff changeset
   199
    decorated_output (*add urgent message annotation*)
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   200
      (special "360") (special "361") ""
16534
wenzelm
parents: 16486
diff changeset
   201
      (assemble_pgips ps)
wenzelm
parents: 16486
diff changeset
   202
  else
wenzelm
parents: 16486
diff changeset
   203
    writeln_default (assemble_pgips ps);
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   204
16534
wenzelm
parents: 16486
diff changeset
   205
fun assemble_pgip resp attrs s = assemble_pgips [XML.element resp attrs [s]];
wenzelm
parents: 16486
diff changeset
   206
fun assemble_pgipe resp attrs = assemble_pgips [XML.element resp attrs []];
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   207
16534
wenzelm
parents: 16486
diff changeset
   208
(* FIXME: need to add stuff to gather PGIPs here *)
wenzelm
parents: 16486
diff changeset
   209
fun issue_pgip resp attrs txt =
wenzelm
parents: 16486
diff changeset
   210
  if pgip_emacs_compatibility () then
wenzelm
parents: 16486
diff changeset
   211
    decorated_output (*add urgent message annotation*)
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   212
      (special "360") (special "361") ""
16534
wenzelm
parents: 16486
diff changeset
   213
      (assemble_pgip resp attrs txt)
wenzelm
parents: 16486
diff changeset
   214
  else
wenzelm
parents: 16486
diff changeset
   215
    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
   216
16534
wenzelm
parents: 16486
diff changeset
   217
(* FIXME: temporarily to support PG 3.4 *)
wenzelm
parents: 16486
diff changeset
   218
fun issue_pgip_maybe_decorated bg en resp attrs s =
wenzelm
parents: 16486
diff changeset
   219
  if pgip_emacs_compatibility () then
wenzelm
parents: 16486
diff changeset
   220
    (*in PGIP mode, but using escape characters as well*)
wenzelm
parents: 16486
diff changeset
   221
    writeln_default (enclose bg en (assemble_pgip resp attrs s))
wenzelm
parents: 16486
diff changeset
   222
  else
wenzelm
parents: 16486
diff changeset
   223
    issue_pgip resp attrs s;
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   224
16534
wenzelm
parents: 16486
diff changeset
   225
fun issue_pgipe resp attrs = writeln_default (assemble_pgipe resp attrs);
wenzelm
parents: 16486
diff changeset
   226
wenzelm
parents: 16486
diff changeset
   227
end;
wenzelm
parents: 16486
diff changeset
   228
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   229
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   230
(* messages and notification *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   231
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
   232
local
16534
wenzelm
parents: 16486
diff changeset
   233
  val delay_msgs = ref false;   (*true: accumulate messages*)
wenzelm
parents: 16486
diff changeset
   234
  val delayed_msgs = ref [];
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
   235
in
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   236
16534
wenzelm
parents: 16486
diff changeset
   237
fun message resp attrs bg en prfx s =
wenzelm
parents: 16486
diff changeset
   238
  if pgip () then
wenzelm
parents: 16486
diff changeset
   239
   (if (! delay_msgs) then
wenzelm
parents: 16486
diff changeset
   240
      delayed_msgs := (resp, attrs, prefix_lines prfx s) :: ! delayed_msgs (*NB: no decs*)
wenzelm
parents: 16486
diff changeset
   241
    else
wenzelm
parents: 16486
diff changeset
   242
      issue_pgip_maybe_decorated bg en resp attrs
wenzelm
parents: 16486
diff changeset
   243
        (XML.element "pgmltext" [] [prefix_lines prfx s]))
wenzelm
parents: 16486
diff changeset
   244
  else decorated_output bg en prfx s;
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
   245
16534
wenzelm
parents: 16486
diff changeset
   246
fun start_delay_msgs () = (set delay_msgs; delayed_msgs := []);
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
   247
16534
wenzelm
parents: 16486
diff changeset
   248
fun end_delayed_msgs () = (reset delay_msgs;
wenzelm
parents: 16486
diff changeset
   249
  (! delayed_msgs) |> map (fn (resp, attrs, s) =>
wenzelm
parents: 16486
diff changeset
   250
    XML.element resp attrs [XML.element "pgmltext" [] [s]]));
wenzelm
parents: 16486
diff changeset
   251
wenzelm
parents: 16486
diff changeset
   252
end;
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   253
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   254
local
16534
wenzelm
parents: 16486
diff changeset
   255
  val display_area = ("area", "display");
wenzelm
parents: 16486
diff changeset
   256
  val message_area = ("area", "message");
wenzelm
parents: 16486
diff changeset
   257
  val internal_category = ("messagecategory", "internal");
wenzelm
parents: 16486
diff changeset
   258
  val info_category = ("messagecategory", "information");
wenzelm
parents: 16486
diff changeset
   259
  val tracing_category = ("messagecategory", "tracing");
wenzelm
parents: 16486
diff changeset
   260
  val urgent_indication = ("urgent", "y");
wenzelm
parents: 16486
diff changeset
   261
  val nonfatal = ("fatality", "nonfatal");
wenzelm
parents: 16486
diff changeset
   262
  val fatal = ("fatality", "fatal");
wenzelm
parents: 16486
diff changeset
   263
  val panic = ("fatality", "panic");
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   264
16534
wenzelm
parents: 16486
diff changeset
   265
  val thyname_attr = pair "thyname";
wenzelm
parents: 16486
diff changeset
   266
  val url_attr = pair "url";
wenzelm
parents: 16486
diff changeset
   267
  fun localfile_url_attr path = url_attr ("file:///" ^ path);
wenzelm
parents: 16486
diff changeset
   268
in
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   269
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   270
fun setup_messages () =
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   271
 (writeln_fn := (fn s => message "normalresponse" [message_area] "" "" "" s);
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   272
  priority_fn := (fn s => message "normalresponse" [message_area, urgent_indication]
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   273
    (special "360") (special "361") "" s);
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   274
  tracing_fn := (fn s => message "normalresponse"  [message_area, tracing_category]
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   275
    (special "360" ^ special "375") (special "361") "" s);
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   276
  info_fn := (fn s => message "normalresponse" [message_area, info_category]
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   277
    (special "362") (special "363") "+++ " s);
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   278
  debug_fn := (fn s => message "normalresponse" [message_area, internal_category]
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   279
    (special "362") (special "363") "+++ " s);
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   280
  warning_fn := (fn s => message "errorresponse" [nonfatal]
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   281
    (special "362") (special "363") "### " s);
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   282
  error_fn := (fn s => message "errorresponse" [fatal]
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   283
    (special "364") (special "365") "*** " s);
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   284
  panic_fn := (fn s => message "errorresponse" [panic]
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   285
    (special "364") (special "365") "!!! " s));
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   286
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   287
15400
50bbdabd7326 Insert pgmltext element into responses in PGIP mode
aspinall
parents: 15289
diff changeset
   288
(* accumulate printed output in a single PGIP response (inside <pgmltext>) *)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   289
16534
wenzelm
parents: 16486
diff changeset
   290
fun with_displaywrap (elt, attrs) dispfn =
wenzelm
parents: 16486
diff changeset
   291
  let
wenzelm
parents: 16486
diff changeset
   292
    val lines = ref ([]: string list);
wenzelm
parents: 16486
diff changeset
   293
    fun wlgrablines s = lines := s :: ! lines;
wenzelm
parents: 16486
diff changeset
   294
  in
wenzelm
parents: 16486
diff changeset
   295
    setmp writeln_fn wlgrablines dispfn ();
16798
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
   296
    (* IMPORTANT FIXME: XML.element here too inefficient, should use stream output *)
16534
wenzelm
parents: 16486
diff changeset
   297
    issue_pgip elt attrs (XML.element "pgmltext" [] (! lines))
wenzelm
parents: 16486
diff changeset
   298
  end;
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   299
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   300
fun emacs_notify s = decorated_output (special "360") (special "361") "" s;
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   301
16534
wenzelm
parents: 16486
diff changeset
   302
fun tell_clear_goals () =
wenzelm
parents: 16486
diff changeset
   303
  if pgip () then
wenzelm
parents: 16486
diff changeset
   304
    issue_pgipe "cleardisplay" [display_area]
wenzelm
parents: 16486
diff changeset
   305
  else
wenzelm
parents: 16486
diff changeset
   306
    emacs_notify "Proof General, please clear the goals buffer.";
wenzelm
parents: 16486
diff changeset
   307
wenzelm
parents: 16486
diff changeset
   308
fun tell_clear_response () =
wenzelm
parents: 16486
diff changeset
   309
  if pgip () then
wenzelm
parents: 16486
diff changeset
   310
    issue_pgipe "cleardisplay" [message_area]
wenzelm
parents: 16486
diff changeset
   311
  else
wenzelm
parents: 16486
diff changeset
   312
    emacs_notify "Proof General, please clear the response buffer.";
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   313
16534
wenzelm
parents: 16486
diff changeset
   314
fun tell_file_loaded path =
wenzelm
parents: 16486
diff changeset
   315
  if pgip () then
16788
0c6f5fe30676 Fix informtheoryloaded/retracted -> informfileloaded/retracted to match pgip.rnc
aspinall
parents: 16534
diff changeset
   316
    issue_pgipe "informfileloaded"
0c6f5fe30676 Fix informtheoryloaded/retracted -> informfileloaded/retracted to match pgip.rnc
aspinall
parents: 16534
diff changeset
   317
      [localfile_url_attr  (XML.text (File.platform_path path))]
16534
wenzelm
parents: 16486
diff changeset
   318
  else
wenzelm
parents: 16486
diff changeset
   319
    emacs_notify ("Proof General, this file is loaded: " ^ quote (File.platform_path path));
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   320
16534
wenzelm
parents: 16486
diff changeset
   321
fun tell_file_retracted path =
wenzelm
parents: 16486
diff changeset
   322
  if pgip() then
16788
0c6f5fe30676 Fix informtheoryloaded/retracted -> informfileloaded/retracted to match pgip.rnc
aspinall
parents: 16534
diff changeset
   323
    issue_pgipe "informfileretracted"
0c6f5fe30676 Fix informtheoryloaded/retracted -> informfileloaded/retracted to match pgip.rnc
aspinall
parents: 16534
diff changeset
   324
      [localfile_url_attr  (XML.text (File.platform_path path))]
16534
wenzelm
parents: 16486
diff changeset
   325
  else
wenzelm
parents: 16486
diff changeset
   326
    emacs_notify ("Proof General, you can unlock the file " ^ quote (File.platform_path path));
12778
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
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   329
(* theory / proof state output *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   330
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   331
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   332
16534
wenzelm
parents: 16486
diff changeset
   333
fun tmp_markers f =
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   334
  setmp Display.current_goals_markers (special "366", special "367", "") f ();
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   335
16534
wenzelm
parents: 16486
diff changeset
   336
fun statedisplay prts =
wenzelm
parents: 16486
diff changeset
   337
  issue_pgip "proofstate" []
wenzelm
parents: 16486
diff changeset
   338
    (XML.element "pgml" []
wenzelm
parents: 16486
diff changeset
   339
      [XML.element "statedisplay" [] [Pretty.output (Pretty.chunks prts)]]);
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   340
16534
wenzelm
parents: 16486
diff changeset
   341
fun print_current_goals n m st =
wenzelm
parents: 16486
diff changeset
   342
  if pgml () then statedisplay (Display.pretty_current_goals n m st)
wenzelm
parents: 16486
diff changeset
   343
  else tmp_markers (fn () => Display.print_current_goals_default n m st);
13545
fcdbd6cf5f9f improved tell_thm_deps;
wenzelm
parents: 13538
diff changeset
   344
16534
wenzelm
parents: 16486
diff changeset
   345
fun print_state b st =
wenzelm
parents: 16486
diff changeset
   346
  if pgml () then statedisplay (Toplevel.pretty_state b st)
wenzelm
parents: 16486
diff changeset
   347
  else tmp_markers (fn () => Toplevel.print_state_default b st);
wenzelm
parents: 16486
diff changeset
   348
13526
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   349
in
9269275e5da6 result dependency output;
wenzelm
parents: 13391
diff changeset
   350
16534
wenzelm
parents: 16486
diff changeset
   351
fun setup_state () =
wenzelm
parents: 16486
diff changeset
   352
  (Display.print_current_goals_fn := print_current_goals;
wenzelm
parents: 16486
diff changeset
   353
   Toplevel.print_state_fn := print_state;
wenzelm
parents: 16486
diff changeset
   354
   (* FIXME: check next octal char won't appear in pgip? *)
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   355
   Toplevel.prompt_state_fn := (fn s => suffix (special "372")
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   356
     (Toplevel.prompt_state_default s)));
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   357
16534
wenzelm
parents: 16486
diff changeset
   358
end;
wenzelm
parents: 16486
diff changeset
   359
wenzelm
parents: 16486
diff changeset
   360
end;
13728
8004e56204fd Added some functions for processing PGIP (thanks to David Aspinall).
berghofe
parents: 13646
diff changeset
   361
16022
96a9bf7ac18d FindTheorems.print_theorems;
wenzelm
parents: 15992
diff changeset
   362
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   363
(* misc commands for ProofGeneral/isa *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   364
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   365
fun thms_containing ss =
16534
wenzelm
parents: 16486
diff changeset
   366
  FindTheorems.print_theorems (ProofContext.init (the_context ())) NONE NONE
16022
96a9bf7ac18d FindTheorems.print_theorems;
wenzelm
parents: 15992
diff changeset
   367
    (map (fn s => (true, FindTheorems.Pattern s)) ss);
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   368
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   369
val welcome = priority o Session.welcome;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   370
val help = welcome;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   371
val show_context = Context.the_context;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   372
17959
8db36a108213 OldGoals;
wenzelm
parents: 17739
diff changeset
   373
fun kill_goal () = (OldGoals.reset_goals (); tell_clear_goals ());
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   374
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   375
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
   376
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   377
fun repeat_undo 0 = ()
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   378
  | repeat_undo 1 = undo ()
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   379
  | 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
   380
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   381
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   382
(* theory loader actions *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   383
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   384
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   385
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   386
fun add_master_files name files =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   387
  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
   388
  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
   389
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   390
fun trace_action action name =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   391
  if action = ThyInfo.Update then
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   392
    List.app tell_file_loaded (ThyInfo.loaded_files name)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   393
  else if action = ThyInfo.Outdate orelse action = ThyInfo.Remove then
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   394
    List.app tell_file_retracted (add_master_files name (ThyInfo.loaded_files name))
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   395
  else ();
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
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   398
  fun setup_thy_loader () = ThyInfo.add_hook trace_action;
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   399
  fun sync_thy_loader () = List.app (trace_action ThyInfo.Update) (ThyInfo.names ());
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   400
end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   401
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   402
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   403
(* prepare theory context *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   404
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   405
val thy_name = Path.pack o #1 o Path.split_ext o Path.base o Path.unpack;
16534
wenzelm
parents: 16486
diff changeset
   406
wenzelm
parents: 16486
diff changeset
   407
(* FIXME general treatment of tracing*)
wenzelm
parents: 16486
diff changeset
   408
val update_thy_only = setmp MetaSimplifier.trace_simp false ThyInfo.update_thy_only;
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   409
16440
9b6e6d5fba05 Context.theory_name;
wenzelm
parents: 16259
diff changeset
   410
fun dynamic_context () =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   411
  (case Context.get_context () of
16440
9b6e6d5fba05 Context.theory_name;
wenzelm
parents: 16259
diff changeset
   412
    SOME thy => "  Using current (dynamic!) one: " ^ quote (Context.theory_name thy)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   413
  | NONE => "");
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   414
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   415
fun try_update_thy_only file =
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   416
  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
   417
    let val name = thy_name file in
16534
wenzelm
parents: 16486
diff changeset
   418
      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
   419
      then update_thy_only name
16440
9b6e6d5fba05 Context.theory_name;
wenzelm
parents: 16259
diff changeset
   420
      else warning ("Unkown theory context of ML file." ^ dynamic_context ())
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   421
    end) ();
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   422
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   423
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   424
(* get informed about files *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   425
16534
wenzelm
parents: 16486
diff changeset
   426
val inform_file_retracted = ThyInfo.if_known_thy ThyInfo.remove_thy o thy_name;
wenzelm
parents: 16486
diff changeset
   427
val inform_file_processed = ThyInfo.if_known_thy ThyInfo.touch_child_thys o thy_name;
wenzelm
parents: 16486
diff changeset
   428
val openfile_retract = Output.no_warnings (ThyInfo.if_known_thy ThyInfo.remove_thy) o thy_name;
15629
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   429
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   430
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
   431
  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
   432
    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
   433
     (ThyInfo.touch_child_thys name;
18678
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18587
diff changeset
   434
      ThyInfo.pretend_use_thy_only name handle ERROR msg =>
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   435
       (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
   436
        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
   437
    else raise Toplevel.UNDEF
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   438
  end;
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
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
   441
 (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
   442
  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
   443
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   444
12778
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   445
(* restart top-level loop (keeps most state information) *)
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   446
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   447
local
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   448
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   449
fun restart isar =
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   450
 (if isar then tell_clear_goals () else kill_goal ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   451
  tell_clear_response ();
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   452
  welcome ());
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   453
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   454
in
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   455
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   456
fun isa_restart () = restart false;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   457
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
   458
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   459
end;
3120e338ffae Interface/proof_general.ML move to proof_general.ML;
wenzelm
parents:
diff changeset
   460
12833
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   461
fun full_proofs true = proofs := 2
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   462
  | full_proofs false = proofs := 1;
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   463
9f3226cfe021 full_proofs;
wenzelm
parents: 12780
diff changeset
   464
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   465
(* theorem dependency output *)
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
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   468
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   469
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
   470
16789
e8f7a6ec92e5 Note about theorem dependencies including themselves.
aspinall
parents: 16788
diff changeset
   471
(* FIXME: investigate why dependencies at the moment include themselves! *)
16534
wenzelm
parents: 16486
diff changeset
   472
fun thm_deps_message (thms, deps) =
wenzelm
parents: 16486
diff changeset
   473
  if pgip() then
wenzelm
parents: 16486
diff changeset
   474
    issue_pgips
wenzelm
parents: 16486
diff changeset
   475
      [XML.element
wenzelm
parents: 16486
diff changeset
   476
        "metainforesponse"  (* FIXME: get thy name from info here? *)
wenzelm
parents: 16486
diff changeset
   477
        [("infotype", "isabelle_theorem_dependencies")]
wenzelm
parents: 16486
diff changeset
   478
        [XML.element "value" [("name", "thms")] [XML.text thms],
wenzelm
parents: 16486
diff changeset
   479
         XML.element "value" [("name", "deps")] [XML.text deps]]]
wenzelm
parents: 16486
diff changeset
   480
  else emacs_notify ("Proof General, theorem dependencies of " ^ thms ^ " are " ^ deps);
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   481
16534
wenzelm
parents: 16486
diff changeset
   482
fun tell_thm_deps ths = conditional (Output.has_mode thm_depsN) (fn () =>
wenzelm
parents: 16486
diff changeset
   483
  let
wenzelm
parents: 16486
diff changeset
   484
    val names = filter_out (equal "") (map Thm.name_of_thm ths);
wenzelm
parents: 16486
diff changeset
   485
    val deps = filter_out (equal "")
17018
1e9e0f5877f2 Adapted to new interface of thms_of_proof.
berghofe
parents: 16958
diff changeset
   486
      (Symtab.keys (fold Proofterm.thms_of_proof
1e9e0f5877f2 Adapted to new interface of thms_of_proof.
berghofe
parents: 16958
diff changeset
   487
        (map Thm.proof_of ths) Symtab.empty));
16534
wenzelm
parents: 16486
diff changeset
   488
  in
wenzelm
parents: 16486
diff changeset
   489
    if null names orelse null deps then ()
wenzelm
parents: 16486
diff changeset
   490
    else thm_deps_message (spaces_quote names, spaces_quote deps)
wenzelm
parents: 16486
diff changeset
   491
  end);
15134
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
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   494
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   495
fun setup_present_hook () =
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
   496
  Present.add_hook (fn _ => fn res => tell_thm_deps (List.concat (map #2 res)));
15134
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
end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   499
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   500
16534
wenzelm
parents: 16486
diff changeset
   501
wenzelm
parents: 16486
diff changeset
   502
(** preferences **)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   503
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   504
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   505
16534
wenzelm
parents: 16486
diff changeset
   506
val pgipnat = XML.element "pgipint" [("min", "0")] [];
wenzelm
parents: 16486
diff changeset
   507
fun pgipnatmax max = XML.element "pgipint" [("min", "0"), ("max", string_of_int max)] [];
wenzelm
parents: 16486
diff changeset
   508
val pgipbool = XML.element "pgipbool" [] [];
wenzelm
parents: 16486
diff changeset
   509
wenzelm
parents: 16486
diff changeset
   510
fun with_default f = (f (), f);
wenzelm
parents: 16486
diff changeset
   511
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   512
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   513
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   514
fun nat_option r = (pgipnat,
16534
wenzelm
parents: 16486
diff changeset
   515
  with_default (fn () => string_of_int (! r)),
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   516
  (fn s => (case Syntax.read_nat s of
16534
wenzelm
parents: 16486
diff changeset
   517
      NONE => error ("nat_option: illegal value: " ^ s)
wenzelm
parents: 16486
diff changeset
   518
    | SOME i => r := i)));
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   519
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   520
fun bool_option r = (pgipbool,
16534
wenzelm
parents: 16486
diff changeset
   521
  with_default (fn () => Bool.toString (! r)),
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   522
  (fn "false" => r := false | "true" => r := true
16534
wenzelm
parents: 16486
diff changeset
   523
    | 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
   524
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   525
val proof_option = (pgipbool,
16534
wenzelm
parents: 16486
diff changeset
   526
  with_default (fn () => Bool.toString (! proofs >= 2)),
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   527
  (fn "false" => proofs := 1 | "true" => proofs := 2
16534
wenzelm
parents: 16486
diff changeset
   528
    | 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
   529
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   530
val thm_deps_option = (pgipbool,
16534
wenzelm
parents: 16486
diff changeset
   531
  with_default (fn () => Bool.toString (Output.has_mode thm_depsN)),
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   532
  (fn "false" => change print_mode (remove (op =) thm_depsN)
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   533
    | "true" => change print_mode (insert (op =) thm_depsN)
16534
wenzelm
parents: 16486
diff changeset
   534
    | 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
   535
16534
wenzelm
parents: 16486
diff changeset
   536
local
wenzelm
parents: 16486
diff changeset
   537
  val pg_print_depth_val = ref 10;
wenzelm
parents: 16486
diff changeset
   538
  fun pg_print_depth n = (print_depth n; pg_print_depth_val := n)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   539
in
16534
wenzelm
parents: 16486
diff changeset
   540
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   541
val print_depth_option = (pgipnat,
16534
wenzelm
parents: 16486
diff changeset
   542
  with_default (fn () => string_of_int (! pg_print_depth_val)),
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   543
  (fn s => (case Syntax.read_nat s of
16534
wenzelm
parents: 16486
diff changeset
   544
      NONE => error ("print_depth_option: illegal value: " ^ s)
wenzelm
parents: 16486
diff changeset
   545
    | SOME i => pg_print_depth i)));
wenzelm
parents: 16486
diff changeset
   546
end;
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   547
16534
wenzelm
parents: 16486
diff changeset
   548
val preferences = ref
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   549
  [("Display",
16534
wenzelm
parents: 16486
diff changeset
   550
    [("show-types",
wenzelm
parents: 16486
diff changeset
   551
      ("Include types in display of Isabelle terms",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   552
       bool_option show_types)),
16534
wenzelm
parents: 16486
diff changeset
   553
     ("show-sorts",
wenzelm
parents: 16486
diff changeset
   554
      ("Include sorts in display of Isabelle terms",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   555
       bool_option show_sorts)),
16534
wenzelm
parents: 16486
diff changeset
   556
     ("show-consts",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   557
      ("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
   558
       bool_option show_consts)),
16534
wenzelm
parents: 16486
diff changeset
   559
     ("long-names",
wenzelm
parents: 16486
diff changeset
   560
      ("Show fully qualified names in Isabelle terms",
wenzelm
parents: 16486
diff changeset
   561
       bool_option long_names)),
wenzelm
parents: 16486
diff changeset
   562
     ("show-brackets",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   563
      ("Show full bracketing in Isabelle terms",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   564
       bool_option show_brackets)),
16534
wenzelm
parents: 16486
diff changeset
   565
     ("show-main-goal",
wenzelm
parents: 16486
diff changeset
   566
      ("Show main goal in proof state display",
wenzelm
parents: 16486
diff changeset
   567
       bool_option Proof.show_main_goal)),
wenzelm
parents: 16486
diff changeset
   568
     ("eta-contract",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   569
      ("Print terms eta-contracted",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   570
       bool_option Syntax.eta_contract))]),
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   571
   ("Advanced Display",
16534
wenzelm
parents: 16486
diff changeset
   572
    [("goals-limit",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   573
      ("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
   574
       nat_option goals_limit)),
16534
wenzelm
parents: 16486
diff changeset
   575
     ("prems-limit",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   576
      ("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
   577
       nat_option ProofContext.prems_limit)),
16534
wenzelm
parents: 16486
diff changeset
   578
     ("print-depth",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   579
      ("Setting for the ML print depth",
15472
4674102737e9 Added show_var_qmarks flag.
berghofe
parents: 15457
diff changeset
   580
       print_depth_option)),
15985
f00dd5e06ffe renamed show_var_qmarks to show_question_marks;
wenzelm
parents: 15964
diff changeset
   581
     ("show-question-marks",
15472
4674102737e9 Added show_var_qmarks flag.
berghofe
parents: 15457
diff changeset
   582
      ("Show leading question mark of variable name",
15985
f00dd5e06ffe renamed show_var_qmarks to show_question_marks;
wenzelm
parents: 15964
diff changeset
   583
       bool_option show_question_marks))]),
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   584
   ("Tracing",
16534
wenzelm
parents: 16486
diff changeset
   585
    [("trace-simplifier",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   586
      ("Trace simplification rules.",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   587
       bool_option trace_simp)),
17417
c56f4809fc6d TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17407
diff changeset
   588
     ("trace-simplifier-depth",
c56f4809fc6d TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17407
diff changeset
   589
      ("Trace simplifier depth limit.",
c56f4809fc6d TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17407
diff changeset
   590
       nat_option trace_simp_depth_limit)),
16534
wenzelm
parents: 16486
diff changeset
   591
     ("trace-rules",
wenzelm
parents: 16486
diff changeset
   592
      ("Trace application of the standard rules",
wenzelm
parents: 16486
diff changeset
   593
       bool_option trace_rules)),
wenzelm
parents: 16486
diff changeset
   594
     ("trace-unification",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   595
      ("Output error diagnostics during unification",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   596
       bool_option Pattern.trace_unify_fail)),
16534
wenzelm
parents: 16486
diff changeset
   597
     ("global-timing",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   598
      ("Whether to enable timing in Isabelle.",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   599
       bool_option Output.timing))]),
16534
wenzelm
parents: 16486
diff changeset
   600
   ("Proof",
wenzelm
parents: 16486
diff changeset
   601
    [("quick-and-dirty",
wenzelm
parents: 16486
diff changeset
   602
      ("Take a few short cuts",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   603
       bool_option quick_and_dirty)),
16534
wenzelm
parents: 16486
diff changeset
   604
     ("full-proofs",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   605
      ("Record full proof objects internally",
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   606
       proof_option)),
16534
wenzelm
parents: 16486
diff changeset
   607
     ("theorem-dependencies",
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   608
       ("Track theorem dependencies within Proof General",
16534
wenzelm
parents: 16486
diff changeset
   609
        thm_deps_option)),
wenzelm
parents: 16486
diff changeset
   610
     ("skip-proofs",
16816
ccf39b7ca3b7 tuned msg;
wenzelm
parents: 16798
diff changeset
   611
      ("Ignore proof scripts (interactive-only)",
15238
cb559bd0b03c Added entry in Settings menu for Toplevel.skip_proofs flag.
berghofe
parents: 15225
diff changeset
   612
       bool_option Toplevel.skip_proofs))])
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   613
   ];
16534
wenzelm
parents: 16486
diff changeset
   614
end;
wenzelm
parents: 16486
diff changeset
   615
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   616
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   617
(* Configuration: GUI config, proverinfo messages *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   618
17732
5b71bef7ad10 Initialise pgip id also for Emacs mode. Allow dynamic config file location for PGIP.
aspinall
parents: 17523
diff changeset
   619
5b71bef7ad10 Initialise pgip id also for Emacs mode. Allow dynamic config file location for PGIP.
aspinall
parents: 17523
diff changeset
   620
fun orenv v d = case (getenv v) of "" => d  | s => s
5b71bef7ad10 Initialise pgip id also for Emacs mode. Allow dynamic config file location for PGIP.
aspinall
parents: 17523
diff changeset
   621
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   622
local
17732
5b71bef7ad10 Initialise pgip id also for Emacs mode. Allow dynamic config file location for PGIP.
aspinall
parents: 17523
diff changeset
   623
    fun config_file()  = orenv "ISABELLE_PGIPCONFIG" "~~/lib/ProofGeneral/pgip_isar.xml"
5b71bef7ad10 Initialise pgip id also for Emacs mode. Allow dynamic config file location for PGIP.
aspinall
parents: 17523
diff changeset
   624
    fun isabelle_www() = orenv "ISABELLE_HOMEPAGE" "http://isabelle.in.tum.de/"
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   625
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   626
fun send_pgip_config () =
16534
wenzelm
parents: 16486
diff changeset
   627
    let
17732
5b71bef7ad10 Initialise pgip id also for Emacs mode. Allow dynamic config file location for PGIP.
aspinall
parents: 17523
diff changeset
   628
        val path = Path.unpack (config_file())
16534
wenzelm
parents: 16486
diff changeset
   629
        val exists = File.exists path
wenzelm
parents: 16486
diff changeset
   630
        val proverinfo =
wenzelm
parents: 16486
diff changeset
   631
            XML.element "proverinfo"
17732
5b71bef7ad10 Initialise pgip id also for Emacs mode. Allow dynamic config file location for PGIP.
aspinall
parents: 17523
diff changeset
   632
              [("name",     	 "Isabelle"), 
5b71bef7ad10 Initialise pgip id also for Emacs mode. Allow dynamic config file location for PGIP.
aspinall
parents: 17523
diff changeset
   633
	       ("version",  	 version),
5b71bef7ad10 Initialise pgip id also for Emacs mode. Allow dynamic config file location for PGIP.
aspinall
parents: 17523
diff changeset
   634
	       ("instance", 	 Session.name()), 
17739
eddebb044a62 Move welcomemsg and helpdoc to pgip_isar.xml
aspinall
parents: 17732
diff changeset
   635
	       ("descr",	 "The Isabelle/Isar theorem prover"),
17732
5b71bef7ad10 Initialise pgip id also for Emacs mode. Allow dynamic config file location for PGIP.
aspinall
parents: 17523
diff changeset
   636
	       ("url",      	 isabelle_www()),   
5b71bef7ad10 Initialise pgip id also for Emacs mode. Allow dynamic config file location for PGIP.
aspinall
parents: 17523
diff changeset
   637
	       ("filenameextns", ".thy;")]
17739
eddebb044a62 Move welcomemsg and helpdoc to pgip_isar.xml
aspinall
parents: 17732
diff changeset
   638
            []
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   639
    in
16534
wenzelm
parents: 16486
diff changeset
   640
        if exists then
wenzelm
parents: 16486
diff changeset
   641
            (issue_pgips [proverinfo]; issue_pgips [File.read path])
18678
dd0c569fa43d sane ERROR handling;
wenzelm
parents: 18587
diff changeset
   642
        else Output.panic ("PGIP configuration file \"" ^ config_file() ^ "\" not found")
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   643
    end;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   644
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   645
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   646
15629
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   647
(* Reveal some information about prover state *)
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   648
fun send_informguise (openfile, opentheory, openproofpos) =
16534
wenzelm
parents: 16486
diff changeset
   649
    let val guisefile =
wenzelm
parents: 16486
diff changeset
   650
            case openfile of SOME f => [XML.element "guisefile"
wenzelm
parents: 16486
diff changeset
   651
                                                    [("url",Url.pack (Url.File (Path.unpack f)))] []]
wenzelm
parents: 16486
diff changeset
   652
                           | _ => []
wenzelm
parents: 16486
diff changeset
   653
        val guisetheory =
wenzelm
parents: 16486
diff changeset
   654
            case opentheory of SOME t => [XML.element "guisetheory" [("thyname", t)] []]
wenzelm
parents: 16486
diff changeset
   655
                             | _ => []
wenzelm
parents: 16486
diff changeset
   656
        val guiseproof =
wenzelm
parents: 16486
diff changeset
   657
            case openproofpos of SOME i => [XML.element "guiseproof" [("proofpos", string_of_int i)] []]
wenzelm
parents: 16486
diff changeset
   658
                               | _ => []
wenzelm
parents: 16486
diff changeset
   659
    in
wenzelm
parents: 16486
diff changeset
   660
        issue_pgips [XML.element "informguise" [] (guisefile @ guisetheory @ guiseproof)]
wenzelm
parents: 16486
diff changeset
   661
    end
15629
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   662
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   663
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   664
(* PGIP identifier tables (prover objects). [incomplete] *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   665
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   666
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   667
    val objtype_thy  = "theory"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   668
    val objtype_thm  = "theorem"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   669
    val objtype_term = "term"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   670
    val objtype_type = "type"
16534
wenzelm
parents: 16486
diff changeset
   671
wenzelm
parents: 16486
diff changeset
   672
    fun xml_idtable ty ctx ids =
wenzelm
parents: 16486
diff changeset
   673
        let
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   674
            fun ctx_attr (SOME c)= [("context", c)]
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   675
              | ctx_attr NONE    = []
16534
wenzelm
parents: 16486
diff changeset
   676
            fun xmlid x = XML.element "identifier" [] [XML.text x];
wenzelm
parents: 16486
diff changeset
   677
        in
wenzelm
parents: 16486
diff changeset
   678
            XML.element "idtable" (("objtype", ty)::ctx_attr ctx)
wenzelm
parents: 16486
diff changeset
   679
                                  (map xmlid ids)
wenzelm
parents: 16486
diff changeset
   680
        end
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   681
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   682
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   683
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
   684
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
   685
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
   686
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   687
fun delallids ty = setids (xml_idtable ty NONE [])
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   688
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   689
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
   690
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
   691
16534
wenzelm
parents: 16486
diff changeset
   692
fun send_thm_idtable ctx thy =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   693
    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
   694
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   695
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
   696
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   697
(* 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
   698
   & maybe not so useful anyway *)
16534
wenzelm
parents: 16486
diff changeset
   699
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   700
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   701
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   702
(* 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
   703
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   704
local
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   705
 val topthy = Toplevel.theory_of o Toplevel.get_state
16486
1a12cdb6ee6b get_thm(s): Name;
wenzelm
parents: 16440
diff changeset
   706
 fun pthm thy name = print_thm (get_thm thy (Name name))
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   707
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   708
 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
   709
in
16798
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
   710
(* FIXME: add askids for "file" here, which returns single theory with same name *)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   711
fun askids (NONE, SOME "theory")  = send_thy_idtable NONE (ThyInfo.names())
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   712
  | askids (NONE, NONE) =  send_thy_idtable NONE (ThyInfo.names())
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   713
                           (* only theories known in top context *)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   714
  | askids (SOME thy, SOME "theory") = send_thy_idtable (SOME thy) (ThyInfo.get_preds thy)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   715
  | askids (SOME thy, SOME "theorem") = send_thm_idtable (SOME thy) (ThyInfo.get_theory thy)
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   716
  | askids (SOME thy, NONE) = (send_thy_idtable (SOME thy) (ThyInfo.get_preds thy);
16534
wenzelm
parents: 16486
diff changeset
   717
                               send_thm_idtable (SOME thy) (ThyInfo.get_theory thy))
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
   718
  | askids (_, SOME ot) = error ("No objects of type "^(quote ot)^" are available here.")
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   719
16534
wenzelm
parents: 16486
diff changeset
   720
fun showid (_,        "theory", n) =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   721
    with_displaywrap (idvalue "theory" n) (fn ()=>(print_theory (ThyInfo.get_theory n)))
16534
wenzelm
parents: 16486
diff changeset
   722
  | showid (SOME thy, "theorem", t) =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   723
    with_displaywrap (idvalue "theorem" t) (fn ()=>(pthm (ThyInfo.get_theory thy) t))
16534
wenzelm
parents: 16486
diff changeset
   724
  | showid (NONE,     "theorem", t) =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   725
    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
   726
  | 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
   727
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   728
end
15629
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   729
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
   730
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   731
(** Parsing proof scripts without execution **)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   732
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   733
(* Notes.
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   734
   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
   735
   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
   736
   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
   737
   the parsing to extract interesting parts of commands.  The trace of
15254
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   738
   tokens parsed which is now recorded in each transition (added by
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   739
   Markus June '04) helps do this, but the mechanism is still a bad mess.
16534
wenzelm
parents: 16486
diff changeset
   740
15254
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   741
   If we had proper parse trees it would be easy, although having a
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   742
   fixed type of trees might be tricky with Isar's extensible parser.
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   743
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   744
   Probably the best solution is to produce the meta-information at
16534
wenzelm
parents: 16486
diff changeset
   745
   the same time as the parse, for each command, e.g. by recording a
wenzelm
parents: 16486
diff changeset
   746
   list of (name,objtype) pairs which record the bindings created by
wenzelm
parents: 16486
diff changeset
   747
   a command.  This would require changing the interfaces in
wenzelm
parents: 16486
diff changeset
   748
   outer_syntax.ML (or providing new ones),
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   749
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   750
    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
   751
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   752
    val command_withmetainfo: string -> string -> string ->
16534
wenzelm
parents: 16486
diff changeset
   753
      (token list ->
wenzelm
parents: 16486
diff changeset
   754
       ((Toplevel.transition -> Toplevel.transition) * metainfo list) *
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   755
       token list) -> parser
15254
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   756
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   757
   We'd also like to render terms as they appear in output, but this
16534
wenzelm
parents: 16486
diff changeset
   758
   will be difficult because inner syntax is extensible and we don't
15254
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   759
   have the correct syntax to hand when just doing outer parsing
16534
wenzelm
parents: 16486
diff changeset
   760
   without execution.  A reasonable approximation could
15254
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   761
   perhaps be obtained by using the syntax of the current context.
16534
wenzelm
parents: 16486
diff changeset
   762
   However, this would mean more mess trying to pick out terms,
15254
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   763
   so at this stage a more serious change to the Isar functions
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   764
   seems necessary.
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   765
*)
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   766
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   767
local
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   768
    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
   769
    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
   770
    fun empty elt = [XML.element elt [] []]
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   771
15210
4ff917a91e16 Remove double escaping of backslash in PGML. Remove use of character refs in <whitespace>
aspinall
parents: 15208
diff changeset
   772
    fun whitespace str = XML.element "whitespace" [] [XML.text str]
15208
09271a87fbf0 Add filenamextns to prover info. Update doc location. Add whitespace element in parseresult
aspinall
parents: 15192
diff changeset
   773
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   774
    (* 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
   775
    val sync = OuterSyntax.scan "\\<^sync>";
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   776
16534
wenzelm
parents: 16486
diff changeset
   777
    fun named_item_elt_with nameattr toks str elt nameP objtyp =
wenzelm
parents: 16486
diff changeset
   778
        let
wenzelm
parents: 16486
diff changeset
   779
            val name = (fst (nameP (toks@sync)))
wenzelm
parents: 16486
diff changeset
   780
                        handle _ => (error ("Error occurred in name parser for " ^ elt ^
wenzelm
parents: 16486
diff changeset
   781
                                            "(objtype: " ^ objtyp ^ ")");
wenzelm
parents: 16486
diff changeset
   782
                                     "")
wenzelm
parents: 16486
diff changeset
   783
wenzelm
parents: 16486
diff changeset
   784
        in
wenzelm
parents: 16486
diff changeset
   785
            [XML.element elt
wenzelm
parents: 16486
diff changeset
   786
                         ((if name="" then [] else [(nameattr, name)])@
wenzelm
parents: 16486
diff changeset
   787
                          (if objtyp="" then [] else [("objtype", objtyp)]))
wenzelm
parents: 16486
diff changeset
   788
                         ([XML.text str])]
wenzelm
parents: 16486
diff changeset
   789
        end
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   790
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   791
    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
   792
    val thmnamed_item_elt = named_item_elt_with "thmname"
16534
wenzelm
parents: 16486
diff changeset
   793
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   794
    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
   795
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   796
    (* 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
   797
       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
   798
16534
wenzelm
parents: 16486
diff changeset
   799
    val keywords_classification_table = ref (NONE: string Symtab.table option)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   800
16534
wenzelm
parents: 16486
diff changeset
   801
    fun get_keywords_classification_table () =
wenzelm
parents: 16486
diff changeset
   802
        case (!keywords_classification_table) of
17221
6cd180204582 curried_lookup/update;
wenzelm
parents: 17217
diff changeset
   803
          SOME t => t
6cd180204582 curried_lookup/update;
wenzelm
parents: 17217
diff changeset
   804
        | NONE => (let
17417
c56f4809fc6d TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17407
diff changeset
   805
                     val tab = fold (fn (c, _, k, _) => Symtab.update (c, k))
17221
6cd180204582 curried_lookup/update;
wenzelm
parents: 17217
diff changeset
   806
                                    (OuterSyntax.dest_parsers ()) Symtab.empty;
6cd180204582 curried_lookup/update;
wenzelm
parents: 17217
diff changeset
   807
                   in (keywords_classification_table := SOME tab; tab) end)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   808
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   809
16534
wenzelm
parents: 16486
diff changeset
   810
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   811
    fun xmls_of_thy_begin (name,toks,str) = (* see isar_syn.ML/theoryP *)
16534
wenzelm
parents: 16486
diff changeset
   812
        let
wenzelm
parents: 16486
diff changeset
   813
            val ((thyname,imports,files),_) = ThyHeader.args (toks@sync)
wenzelm
parents: 16486
diff changeset
   814
        in
wenzelm
parents: 16486
diff changeset
   815
            markup_text_attrs str "opentheory"
wenzelm
parents: 16486
diff changeset
   816
                              ([("thyname",thyname)] @
wenzelm
parents: 16486
diff changeset
   817
                               (if imports=[] then [] else
wenzelm
parents: 16486
diff changeset
   818
                                [("parentnames", (space_implode ";" imports) ^ ";")]))
wenzelm
parents: 16486
diff changeset
   819
        end
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   820
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   821
    fun xmls_of_thy_decl (name,toks,str) = (* see isar_syn.ML/thy_decl cases  *)
16534
wenzelm
parents: 16486
diff changeset
   822
        let
wenzelm
parents: 16486
diff changeset
   823
            (* NB: PGIP only deals with single name bindings at the moment;
wenzelm
parents: 16486
diff changeset
   824
               potentially we could markup grouped definitions several times but
wenzelm
parents: 16486
diff changeset
   825
               that might suggest the wrong structure to the editor?
wenzelm
parents: 16486
diff changeset
   826
               Better alternative would be to put naming closer around text,
wenzelm
parents: 16486
diff changeset
   827
               but to do that we'd be much better off modifying the real parser
wenzelm
parents: 16486
diff changeset
   828
               instead of reconstructing it here. *)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   829
16534
wenzelm
parents: 16486
diff changeset
   830
            val plain_items = (* no names, unimportant names, or too difficult *)
wenzelm
parents: 16486
diff changeset
   831
                ["defaultsort","arities","judgement","finalconsts",
wenzelm
parents: 16486
diff changeset
   832
                 "syntax", "nonterminals", "translations",
wenzelm
parents: 16486
diff changeset
   833
                 "global", "local", "hide",
wenzelm
parents: 16486
diff changeset
   834
                 "ML_setup", "setup", "method_setup",
wenzelm
parents: 16486
diff changeset
   835
                 "parse_ast_translation", "parse_translation", "print_translation",
wenzelm
parents: 16486
diff changeset
   836
                 "typed_print_translation", "print_ast_translation", "token_translation",
wenzelm
parents: 16486
diff changeset
   837
                 "oracle",
wenzelm
parents: 16486
diff changeset
   838
                 "declare"]
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   839
16534
wenzelm
parents: 16486
diff changeset
   840
            val plain_item   = markup_text str "theoryitem"
wenzelm
parents: 16486
diff changeset
   841
            val comment_item = markup_text str "litcomment"
wenzelm
parents: 16486
diff changeset
   842
            val named_item   = named_item_elt toks str "theoryitem"
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   843
16534
wenzelm
parents: 16486
diff changeset
   844
            val opt_overloaded = P.opt_keyword "overloaded";
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   845
16534
wenzelm
parents: 16486
diff changeset
   846
            val thmnameP = (* see isar_syn.ML/theoremsP *)
wenzelm
parents: 16486
diff changeset
   847
                let
wenzelm
parents: 16486
diff changeset
   848
                    val name_facts = P.and_list1 ((P.opt_thm_name "=" --| P.xthms1) >> #1)
16958
1b4a3110c64a P.opt_locale_target;
wenzelm
parents: 16896
diff changeset
   849
                    val theoremsP = P.opt_locale_target |-- name_facts >> (fn [] => "" | x::_ => x)
16534
wenzelm
parents: 16486
diff changeset
   850
                in
wenzelm
parents: 16486
diff changeset
   851
                    theoremsP
wenzelm
parents: 16486
diff changeset
   852
                end
wenzelm
parents: 16486
diff changeset
   853
        in
wenzelm
parents: 16486
diff changeset
   854
            (* TODO: ideally we would like to render terms properly, just as they are
wenzelm
parents: 16486
diff changeset
   855
               in output. This implies using PGML for symbols and variables/atoms.
wenzelm
parents: 16486
diff changeset
   856
               BUT it's rather tricky without having the correct concrete syntax to hand,
wenzelm
parents: 16486
diff changeset
   857
               and even if we did, we'd have to mess around here a whole lot more first
wenzelm
parents: 16486
diff changeset
   858
               to pick out the terms from the syntax. *)
15254
10cfd6a14682 Simplification to symbol processing; put quotes around theory name in message.
aspinall
parents: 15253
diff changeset
   859
16534
wenzelm
parents: 16486
diff changeset
   860
            if (name mem plain_items) then plain_item
wenzelm
parents: 16486
diff changeset
   861
            else case name of
wenzelm
parents: 16486
diff changeset
   862
                     "text"      => comment_item
wenzelm
parents: 16486
diff changeset
   863
                   | "text_raw"  => comment_item
wenzelm
parents: 16486
diff changeset
   864
                   | "typedecl"  => named_item (P.type_args |-- P.name) "type"
wenzelm
parents: 16486
diff changeset
   865
                   | "types"     => named_item (P.type_args |-- P.name) "type"
wenzelm
parents: 16486
diff changeset
   866
                   | "classes"   => named_item P.name "class"
wenzelm
parents: 16486
diff changeset
   867
                   | "classrel"  => named_item P.name "class"
wenzelm
parents: 16486
diff changeset
   868
                   | "consts"    => named_item (P.const >> #1) "term"
wenzelm
parents: 16486
diff changeset
   869
                   | "axioms"    => named_item (P.spec_name >> (#1 o #1)) "theorem"
wenzelm
parents: 16486
diff changeset
   870
                   | "defs"      => named_item (opt_overloaded |-- P.spec_name >> (#1 o #1)) "theorem"
wenzelm
parents: 16486
diff changeset
   871
                   | "constdefs" => named_item P.name (* FIXME: heavily simplified/wrong *) "term"
wenzelm
parents: 16486
diff changeset
   872
                   | "theorems"  => named_item thmnameP "thmset"
wenzelm
parents: 16486
diff changeset
   873
                   | "lemmas"    => named_item thmnameP "thmset"
wenzelm
parents: 16486
diff changeset
   874
                   | "oracle"    => named_item P.name "oracle"
wenzelm
parents: 16486
diff changeset
   875
                   | "locale"    => named_item ((P.opt_keyword "open" >> not) |-- P.name) "locale"
wenzelm
parents: 16486
diff changeset
   876
                   | _ => (parse_warning ("Unrecognized thy-decl command: " ^ name); plain_item)
wenzelm
parents: 16486
diff changeset
   877
        end
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   878
16534
wenzelm
parents: 16486
diff changeset
   879
    fun xmls_of_thy_goal (name,toks,str) =
wenzelm
parents: 16486
diff changeset
   880
        let
wenzelm
parents: 16486
diff changeset
   881
            (* see isar_syn.ML/gen_theorem *)
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   882
         val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp);
16534
wenzelm
parents: 16486
diff changeset
   883
         val general_statement =
18130
108ed679cf5a P.locale_element;
wenzelm
parents: 17959
diff changeset
   884
            statement >> pair [] || Scan.repeat P.locale_element -- (P.$$$ "shows" |-- statement);
16534
wenzelm
parents: 16486
diff changeset
   885
wenzelm
parents: 16486
diff changeset
   886
            val gen_theoremP =
16958
1b4a3110c64a P.opt_locale_target;
wenzelm
parents: 16896
diff changeset
   887
                P.opt_locale_target -- Scan.optional (P.opt_thm_name ":" --|
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   888
                 Scan.ahead (P.locale_keyword || P.$$$ "shows")) ("", []) --
16534
wenzelm
parents: 16486
diff changeset
   889
                                 general_statement >> (fn ((locale, a), (elems, concl)) =>
wenzelm
parents: 16486
diff changeset
   890
                                                         fst a) (* a : (bstring * Args.src list) *)
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   891
16958
1b4a3110c64a P.opt_locale_target;
wenzelm
parents: 16896
diff changeset
   892
            val nameP = P.opt_locale_target |-- (Scan.optional ((P.opt_thm_name ":") >> #1) "")
16534
wenzelm
parents: 16486
diff changeset
   893
            (* TODO: add preference values for attributes
wenzelm
parents: 16486
diff changeset
   894
               val prefval = XML.element "prefval" [("name","thm-kind"),("value",name)]
wenzelm
parents: 16486
diff changeset
   895
            *)
wenzelm
parents: 16486
diff changeset
   896
        in
wenzelm
parents: 16486
diff changeset
   897
            (thmnamed_item_elt toks str "opengoal" nameP "") @
wenzelm
parents: 16486
diff changeset
   898
            (empty "openblock")
wenzelm
parents: 16486
diff changeset
   899
        end
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
   900
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   901
    fun xmls_of_qed (name,markup) =
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   902
        let val qedmarkup  =
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   903
                (case name of
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   904
                     "sorry" => markup "postponegoal"
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   905
                   | "oops"  => markup "giveupgoal"
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   906
                   | "done"  => markup "closegoal"
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   907
                   | "by"    => markup "closegoal"  (* nested or toplevel *)
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   908
                   | "qed"   => markup "closegoal"  (* nested or toplevel *)
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   909
                   | "."     => markup "closegoal"  (* nested or toplevel *)
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   910
                   | ".."    => markup "closegoal"  (* nested or toplevel *)
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   911
                   | other => (* default to closegoal: may be wrong for extns *)
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   912
                                  (parse_warning
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   913
                                       ("Unrecognized qed command: " ^ quote other);
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   914
                                       markup "closegoal"))
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
   915
        in qedmarkup @ (empty "closeblock") end
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   916
16534
wenzelm
parents: 16486
diff changeset
   917
    fun xmls_of_kind kind (name,toks,str) =
wenzelm
parents: 16486
diff changeset
   918
    let val markup = markup_text str in
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   919
    case kind of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   920
      "control"        => markup "badcmd"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   921
    | "diag"           => markup "spuriouscmd"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   922
    (* theory/files *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   923
    | "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
   924
    | "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
   925
    | "theory-heading" => markup "litcomment"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   926
    | "theory-script"  => markup "theorystep"
15146
eab7de0d0a31 Parsing fixes: extra sync token; thmname attribute in opengoal; theory-end. Comments.
aspinall
parents: 15145
diff changeset
   927
    | "theory-end"     => markup "closetheory"
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   928
    (* proof control *)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   929
    | "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
   930
    | "proof-heading"  => markup "litcomment"
15225
68ab0f4eb457 Add openblock/closeblock to other opengoal/closegoal elements
aspinall
parents: 15220
diff changeset
   931
    | "proof-goal"     => (markup "opengoal") @ (empty "openblock")  (* nested proof: have, show, ... *)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   932
    | "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
   933
    | "proof-open"     => (empty "openblock") @ (markup "proofstep")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   934
    | "proof-close"    => (markup "proofstep") @ (empty "closeblock")
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   935
    | "proof-script"   => markup "proofstep"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   936
    | "proof-chain"    => markup "proofstep"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   937
    | "proof-decl"     => markup "proofstep"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   938
    | "proof-asm"      => markup "proofstep"
15289
1d2dba93ef08 Markup obtain as introducing a nested goal.
aspinall
parents: 15286
diff changeset
   939
    | "proof-asm-goal" => (markup "opengoal") @ (empty "openblock")  (* nested proof: obtain *)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   940
    | "qed"            => xmls_of_qed (name,markup)
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   941
    | "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
   942
    | "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
   943
    | 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
   944
      (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
   945
       markup "spuriouscmd")
16534
wenzelm
parents: 16486
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
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   948
16534
wenzelm
parents: 16486
diff changeset
   949
fun xmls_of_transition (name,str,toks) =
wenzelm
parents: 16486
diff changeset
   950
   let
17417
c56f4809fc6d TableFun/Symtab: curried lookup and update;
wenzelm
parents: 17407
diff changeset
   951
     val classification = Symtab.lookup (get_keywords_classification_table ()) name
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   952
   in case classification of
16534
wenzelm
parents: 16486
diff changeset
   953
          SOME k => (xmls_of_kind k (name,toks,str))
wenzelm
parents: 16486
diff changeset
   954
        | NONE => (* an uncategorized keyword ignored for undo (maybe wrong) *)
wenzelm
parents: 16486
diff changeset
   955
          (parse_warning ("Uncategorized command found: " ^ name ^ " -- using spuriouscmd");
wenzelm
parents: 16486
diff changeset
   956
           markup_text str "spuriouscmd")
wenzelm
parents: 16486
diff changeset
   957
   end
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   958
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   959
fun markup_toks [] _ = []
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   960
  | markup_toks toks x = markup_text (implode (map OuterLex.unparse toks)) x
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   961
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   962
fun markup_comment_whs [] = []
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   963
  | markup_comment_whs (toks as t::ts) = (* this would be a lot neater if we could match on toks! *)
16534
wenzelm
parents: 16486
diff changeset
   964
    let
wenzelm
parents: 16486
diff changeset
   965
        val (prewhs,rest) = take_prefix (OuterLex.is_kind OuterLex.Space) toks
wenzelm
parents: 16486
diff changeset
   966
    in
wenzelm
parents: 16486
diff changeset
   967
        if (prewhs <> []) then
wenzelm
parents: 16486
diff changeset
   968
            whitespace (implode (map OuterLex.unparse prewhs))
wenzelm
parents: 16486
diff changeset
   969
            :: (markup_comment_whs rest)
wenzelm
parents: 16486
diff changeset
   970
        else
wenzelm
parents: 16486
diff changeset
   971
            (markup_text (OuterLex.unparse t) "comment") @
wenzelm
parents: 16486
diff changeset
   972
            (markup_comment_whs ts)
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   973
    end
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   974
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   975
fun xmls_pre_cmd [] = ([],[])
16534
wenzelm
parents: 16486
diff changeset
   976
  | xmls_pre_cmd toks =
wenzelm
parents: 16486
diff changeset
   977
    let
wenzelm
parents: 16486
diff changeset
   978
        (* an extra token is needed to terminate the command *)
wenzelm
parents: 16486
diff changeset
   979
        val sync = OuterSyntax.scan "\\<^sync>";
wenzelm
parents: 16486
diff changeset
   980
        val spaceP = Scan.bulk (Scan.one (fn t =>not (OuterLex.is_proper t)) >> OuterLex.val_of) >> implode
wenzelm
parents: 16486
diff changeset
   981
        val text_with_whs =
wenzelm
parents: 16486
diff changeset
   982
            ((spaceP || Scan.succeed "") --
wenzelm
parents: 16486
diff changeset
   983
             (P.short_ident || P.long_ident || P.sym_ident || P.string || P.number || P.verbatim) >> op^)
wenzelm
parents: 16486
diff changeset
   984
             -- (spaceP || Scan.succeed "") >> op^
wenzelm
parents: 16486
diff changeset
   985
        val (prewhs,rest1) = take_prefix (not o OuterLex.is_proper) (toks@sync)
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   986
        (* NB: this collapses  litcomment,(litcomment|whitespace)* to a single litcomment *)
16534
wenzelm
parents: 16486
diff changeset
   987
        val (_,rest2) = (Scan.bulk (P.$$$ "--" |-- text_with_whs) >> implode || Scan.succeed "") rest1
wenzelm
parents: 16486
diff changeset
   988
        val (postwhs,rest3) = take_prefix (not o OuterLex.is_proper) rest2
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
   989
    in
16534
wenzelm
parents: 16486
diff changeset
   990
        ((markup_comment_whs prewhs) @
wenzelm
parents: 16486
diff changeset
   991
         (if (length rest2 = length rest1)  then []
wenzelm
parents: 16486
diff changeset
   992
          else markup_text (implode
wenzelm
parents: 16486
diff changeset
   993
                                (map OuterLex.unparse (Library.take (length rest1 - length rest2, rest1))))
wenzelm
parents: 16486
diff changeset
   994
               "litcomment") @
wenzelm
parents: 16486
diff changeset
   995
         (markup_comment_whs postwhs),
wenzelm
parents: 16486
diff changeset
   996
         Library.take (length rest3 - 1,rest3))
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   997
    end
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
   998
16534
wenzelm
parents: 16486
diff changeset
   999
fun xmls_of_impropers toks =
wenzelm
parents: 16486
diff changeset
  1000
    let
wenzelm
parents: 16486
diff changeset
  1001
        val (xmls,rest) = xmls_pre_cmd toks
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
  1002
    in
16534
wenzelm
parents: 16486
diff changeset
  1003
        xmls @ (markup_toks rest "unparseable")
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1004
    end
16534
wenzelm
parents: 16486
diff changeset
  1005
wenzelm
parents: 16486
diff changeset
  1006
fun markup_unparseable str = markup_text str "unparseable"
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
  1007
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1008
end
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1009
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1010
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1011
local
16534
wenzelm
parents: 16486
diff changeset
  1012
    (* we have to weave together the whitespace/comments with proper tokens
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1013
       to reconstruct the input. *)
15191
5ca1fd9dec83 Support parsing of -- {* comments *}. Add extra output channels.
aspinall
parents: 15173
diff changeset
  1014
    (* TODO: see if duplicating isar_output/parse_thy can help here *)
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 match_tokens ([],us,vs) = (rev vs,us)  (* used, unused *)
16534
wenzelm
parents: 16486
diff changeset
  1017
      | match_tokens (t::ts,w::ws,vs) =
wenzelm
parents: 16486
diff changeset
  1018
        if (t = w) then match_tokens (ts,ws,w::vs)
wenzelm
parents: 16486
diff changeset
  1019
        else match_tokens (t::ts,ws,w::vs)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1020
      | 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
  1021
in
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1022
    fun xmls_of_str str =
16534
wenzelm
parents: 16486
diff changeset
  1023
    let
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1024
       (* 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
  1025
       fun parse_loop ([],[],xmls) = xmls
16534
wenzelm
parents: 16486
diff changeset
  1026
         | parse_loop ([],itoks,xmls) = xmls @ (xmls_of_impropers itoks)
wenzelm
parents: 16486
diff changeset
  1027
         | parse_loop ((nm,toks,_)::trs,itoks,xmls) =
wenzelm
parents: 16486
diff changeset
  1028
           let
wenzelm
parents: 16486
diff changeset
  1029
               (* first proper token after whitespace/litcomment/whitespace is command *)
wenzelm
parents: 16486
diff changeset
  1030
               val (xmls_pre_cmd,cmditoks') = xmls_pre_cmd itoks
wenzelm
parents: 16486
diff changeset
  1031
               val (cmdtok,itoks') = case cmditoks' of x::xs => (x,xs)
wenzelm
parents: 16486
diff changeset
  1032
                                                     | _ => error("proof_general/parse_loop impossible")
wenzelm
parents: 16486
diff changeset
  1033
               val (utoks,itoks'') = match_tokens (toks,itoks',[])
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1034
               (* 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
  1035
16534
wenzelm
parents: 16486
diff changeset
  1036
               val str = implode (map OuterLex.unparse (cmdtok::utoks))
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1037
16534
wenzelm
parents: 16486
diff changeset
  1038
               val xmls_tr  = xmls_of_transition (nm,str,toks)
wenzelm
parents: 16486
diff changeset
  1039
           in
wenzelm
parents: 16486
diff changeset
  1040
               parse_loop(trs,itoks'',xmls @ xmls_pre_cmd @ xmls_tr)
wenzelm
parents: 16486
diff changeset
  1041
           end
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1042
    in
16534
wenzelm
parents: 16486
diff changeset
  1043
        (let val toks = OuterSyntax.scan str
wenzelm
parents: 16486
diff changeset
  1044
         in
wenzelm
parents: 16486
diff changeset
  1045
             parse_loop (OuterSyntax.read toks, toks, [])
wenzelm
parents: 16486
diff changeset
  1046
         end)
wenzelm
parents: 16486
diff changeset
  1047
           handle _ => markup_unparseable str
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1048
    end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1049
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1050
16534
wenzelm
parents: 16486
diff changeset
  1051
fun parsescript str attrs =
wenzelm
parents: 16486
diff changeset
  1052
    let
wenzelm
parents: 16486
diff changeset
  1053
        val _ = start_delay_msgs ()  (* accumulate error messages to put inside parseresult *)
wenzelm
parents: 16486
diff changeset
  1054
        val xmls = xmls_of_str str
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
  1055
        val errs = end_delayed_msgs ()
16534
wenzelm
parents: 16486
diff changeset
  1056
     in
wenzelm
parents: 16486
diff changeset
  1057
        issue_pgips [XML.element "parseresult" attrs (errs@xmls)]
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
  1058
    end
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1059
end
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1060
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1061
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
(**** PGIP:  Isabelle -> Interface ****)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1064
16534
wenzelm
parents: 16486
diff changeset
  1065
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
  1066
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
  1067
16798
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1068
(* TODO: would be cleaner to define a datatype here for the accepted elements,
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1069
   and mapping functions to/from strings.  At the moment this list must
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1070
   coincide with the strings in the function process_pgip_element. *)
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1071
val isabelle_acceptedpgipelems =
16798
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1072
    ["askpgip","askpgml","askprefs","getpref","setpref",
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1073
     "proverinit","proverexit","startquiet","stopquiet",
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1074
     "pgmlsymbolson", "pgmlsymbolsoff",
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1075
     "dostep", "undostep", "redostep", "abortgoal", "forget", "restoregoal",
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1076
     "askids", "showid", "askguise",
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1077
     "parsescript",
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1078
     "showproofstate", "showctxt", "searchtheorems", "setlinewidth", "viewdoc",
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1079
     "doitem", "undoitem", "redoitem", "abortheory",
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1080
     "retracttheory", "loadfile", "openfile", "closefile",
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1081
     "abortfile", "changecwd", "systemcmd"];
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1082
16534
wenzelm
parents: 16486
diff changeset
  1083
fun usespgip () =
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1084
    issue_pgip
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1085
        "usespgip"
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1086
        [("version", isabelle_pgip_version_supported)]
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1087
        (XML.element "acceptedpgipelems" []
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1088
                     (map (fn s=>XML.element "pgipelem"
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1089
                                             [] (* if threads: possibility to add async here *)
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1090
                                             [s])
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1091
                          isabelle_acceptedpgipelems))
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1092
16534
wenzelm
parents: 16486
diff changeset
  1093
fun usespgml () =
16798
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1094
    issue_pgipe "usespgml" [("version", isabelle_pgml_version_supported)]
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1095
16534
wenzelm
parents: 16486
diff changeset
  1096
fun hasprefs () =
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
  1097
    List.app (fn (prefcat, prefs) =>
16534
wenzelm
parents: 16486
diff changeset
  1098
            issue_pgips [XML.element "hasprefs" [("prefcategory",prefcat)]
wenzelm
parents: 16486
diff changeset
  1099
                 (map (fn (name, (descr, (ty, (default,_),_))) =>
wenzelm
parents: 16486
diff changeset
  1100
                       XML.element "haspref" [("name", name),
wenzelm
parents: 16486
diff changeset
  1101
                                              ("descr", descr),
wenzelm
parents: 16486
diff changeset
  1102
                                              ("default", default)]
16798
36d34186741b Add acceptedpgipelems message
aspinall
parents: 16791
diff changeset
  1103
                       [ty]) prefs)]) (!preferences)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1104
15570
8d8c70b41bab Move towards standard functions.
skalberg
parents: 15531
diff changeset
  1105
fun allprefs () = Library.foldl (op @) ([], map snd (!preferences))
16534
wenzelm
parents: 16486
diff changeset
  1106
wenzelm
parents: 16486
diff changeset
  1107
fun setpref name value =
17314
04e21a27c0ad introduces some modern-style AList operations
haftmann
parents: 17221
diff changeset
  1108
    (case AList.lookup (op =) (allprefs ()) name of
16534
wenzelm
parents: 16486
diff changeset
  1109
         NONE => warning ("Unknown pref: " ^ quote name)
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
  1110
       | SOME (_, (_, _, set)) => set value);
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1111
16534
wenzelm
parents: 16486
diff changeset
  1112
fun getpref name =
17314
04e21a27c0ad introduces some modern-style AList operations
haftmann
parents: 17221
diff changeset
  1113
    (case AList.lookup (op =) (allprefs ()) name of
16534
wenzelm
parents: 16486
diff changeset
  1114
         NONE => warning ("Unknown pref: " ^ quote name)
wenzelm
parents: 16486
diff changeset
  1115
       | SOME (_, (_, (_,get), _)) =>
wenzelm
parents: 16486
diff changeset
  1116
           issue_pgip "prefval" [("name", name)] (get ()));
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1117
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1118
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1119
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1120
(**** PGIP:  Interface -> Isabelle/Isar ****)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1121
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1122
exception PGIP of string;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1123
exception PGIP_QUIT;
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1124
16534
wenzelm
parents: 16486
diff changeset
  1125
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1126
(* Sending commands to Isar *)
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1127
16534
wenzelm
parents: 16486
diff changeset
  1128
fun isarcmd s =
wenzelm
parents: 16486
diff changeset
  1129
    s |> OuterSyntax.scan |> OuterSyntax.read
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1130
      |> 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
  1131
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1132
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
  1133
  | xmltext [] = ""
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1134
  | xmltext _ = raise PGIP "Expected text (PCDATA/CDATA)"
16534
wenzelm
parents: 16486
diff changeset
  1135
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1136
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
  1137
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1138
16791
31678cf364b1 Add management for current working directory
aspinall
parents: 16789
diff changeset
  1139
(* load an arbitrary file (must be .thy or .ML) *)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1140
16534
wenzelm
parents: 16486
diff changeset
  1141
fun use_thy_or_ml_file file =
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1142
    let
16534
wenzelm
parents: 16486
diff changeset
  1143
        val (path,extn) = Path.split_ext (Path.unpack file)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1144
    in
16534
wenzelm
parents: 16486
diff changeset
  1145
        case extn of
wenzelm
parents: 16486
diff changeset
  1146
            "" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
wenzelm
parents: 16486
diff changeset
  1147
          | "thy" => isarcmd ("use_thy " ^ (quote (Path.pack path)))
wenzelm
parents: 16486
diff changeset
  1148
          | "ML" => isarcmd ("use " ^ quote file)
wenzelm
parents: 16486
diff changeset
  1149
          | other => error ("Don't know how to read a file with extension " ^ other)
wenzelm
parents: 16486
diff changeset
  1150
    end
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1151
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1152
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
(* Proof control commands *)
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1154
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
  1155
local
17314
04e21a27c0ad introduces some modern-style AList operations
haftmann
parents: 17221
diff changeset
  1156
  fun xmlattro attr attrs = AList.lookup (op =) attrs attr
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1157
16534
wenzelm
parents: 16486
diff changeset
  1158
  fun xmlattr attr attrs =
wenzelm
parents: 16486
diff changeset
  1159
      (case xmlattro attr attrs of
wenzelm
parents: 16486
diff changeset
  1160
           SOME value => value
wenzelm
parents: 16486
diff changeset
  1161
         | NONE => raise PGIP ("Missing attribute: " ^ attr))
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1162
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
  1163
  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
  1164
  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
  1165
  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
  1166
  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
  1167
  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
  1168
  val dirname_attr = xmlattr "dir"
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1169
  fun comment x = "(* " ^ x ^ " *)"
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1170
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
  1171
  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
  1172
      case Url.unpack url of
16534
wenzelm
parents: 16486
diff changeset
  1173
          (Url.File path) => File.platform_path path
wenzelm
parents: 16486
diff changeset
  1174
        | _ => 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
  1175
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
  1176
  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
  1177
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1178
  val topthy = Toplevel.theory_of o Toplevel.get_state
16440
9b6e6d5fba05 Context.theory_name;
wenzelm
parents: 16259
diff changeset
  1179
  val topthy_name = Context.theory_name o topthy
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1180
15531
08c8dad8e399 Deleted Library.option type.
skalberg
parents: 15472
diff changeset
  1181
  val currently_open_file = ref (NONE : string option)
15629
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
  1182
16791
31678cf364b1 Add management for current working directory
aspinall
parents: 16789
diff changeset
  1183
  (* Path management: we allow theory files to have dependencies
31678cf364b1 Add management for current working directory
aspinall
parents: 16789
diff changeset
  1184
     in their own directory, but when we change directory for a new
31678cf364b1 Add management for current working directory
aspinall
parents: 16789
diff changeset
  1185
     file we remove the path.  Leaving it there can cause confusion
31678cf364b1 Add management for current working directory
aspinall
parents: 16789
diff changeset
  1186
     with difference in batch mode.a  NB: PGIP does not assume
31678cf364b1 Add management for current working directory
aspinall
parents: 16789
diff changeset
  1187
     that the prover has a load path. *)
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1188
  local
16791
31678cf364b1 Add management for current working directory
aspinall
parents: 16789
diff changeset
  1189
      val current_working_dir = ref (NONE : string option)
31678cf364b1 Add management for current working directory
aspinall
parents: 16789
diff changeset
  1190
  in
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1191
      fun changecwd dir =
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1192
          (case (!current_working_dir) of
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1193
               NONE => ()
16791
31678cf364b1 Add management for current working directory
aspinall
parents: 16789
diff changeset
  1194
             | SOME dir => ThyLoad.del_path dir;
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1195
           ThyLoad.add_path dir;
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1196
           current_working_dir := SOME dir)
16791
31678cf364b1 Add management for current working directory
aspinall
parents: 16789
diff changeset
  1197
  end
31678cf364b1 Add management for current working directory
aspinall
parents: 16789
diff changeset
  1198
18587
d4dcdfd764a0 Toplevel.proof_position_of;
wenzelm
parents: 18560
diff changeset
  1199
  fun topproofpos () = try Toplevel.proof_position_of (Isar.state ());
15134
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1200
in
d3fa5e1d6e4d Experimental version supporting PGIP, merged with main branch with help from Makarius.
aspinall
parents: 15010
diff changeset
  1201
16534
wenzelm
parents: 16486
diff changeset
  1202
fun process_pgip_element pgipxml = (case pgipxml of
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1203
  (XML.Text t) => warning ("Ignored text in PGIP packet: \n" ^ t)
16534
wenzelm
parents: 16486
diff changeset
  1204
| (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
  1205
  (case elem of
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1206
       (* protocol config *)
16534
wenzelm
parents: 16486
diff changeset
  1207
       "askpgip"        => (pgip_emacs_compatibility_flag:=false; (* PG>=3.6 or other PGIP interface *)
wenzelm
parents: 16486
diff changeset
  1208
                            usespgip (); send_pgip_config ())
wenzelm
parents: 16486
diff changeset
  1209
     | "askpgml"        => usespgml ()
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1210
     (* proverconfig *)
16534
wenzelm
parents: 16486
diff changeset
  1211
     | "askprefs"       => hasprefs ()
wenzelm
parents: 16486
diff changeset
  1212
     | "getpref"        => getpref (name_attr attrs)
wenzelm
parents: 16486
diff changeset
  1213
     | "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
  1214
     (* provercontrol *)
16534
wenzelm
parents: 16486
diff changeset
  1215
     | "proverinit"     => isar_restart ()
wenzelm
parents: 16486
diff changeset
  1216
     | "proverexit"     => isarcmd "quit"
wenzelm
parents: 16486
diff changeset
  1217
     | "startquiet"     => isarcmd "disable_pr"
wenzelm
parents: 16486
diff changeset
  1218
     | "stopquiet"      => isarcmd "enable_pr"
18174
c6e3c6516a23 pgmlsymbolson: append Symbol.xsymbolsN at end!
wenzelm
parents: 18130
diff changeset
  1219
     | "pgmlsymbolson"   => change print_mode (fn mode =>
c6e3c6516a23 pgmlsymbolson: append Symbol.xsymbolsN at end!
wenzelm
parents: 18130
diff changeset
  1220
          remove (op =) Symbol.xsymbolsN mode @ [Symbol.xsymbolsN])
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1221
     | "pgmlsymbolsoff"  => change print_mode (remove (op =) Symbol.xsymbolsN)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1222
     (* properproofcmd: proper commands which belong in script *)
15401
ba28d103bada Support PGIP <whitespace>, <dostep>, <doitem> elements as input
aspinall
parents: 15400
diff changeset
  1223
     (* FIXME: next ten are by Eclipse interface, can be removed in favour of dostep *)
15629
4066f01f1beb Add askguise/informguise as best as easily possible. Prevent warning in openfile when file doesn't exist in theory database.
aspinall
parents: 15626
diff changeset
  1224
     (* NB: Isar doesn't make lemma name of goal accessible during proof *)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1225
     | "opengoal"       => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1226
     | "proofstep"      => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1227
     | "closegoal"      => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1228
     | "giveupgoal"     => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1229
     | "postponegoal"   => isarscript data
16534
wenzelm
parents: 16486
diff changeset
  1230
     | "comment"        => isarscript data  (* NB: should be ignored, but process anyway *)
wenzelm
parents: 16486
diff changeset
  1231
     | "whitespace"     => isarscript data  (* NB: should be ignored, but process anyway *)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1232
     | "litcomment"     => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1233
     | "spuriouscmd"    => isarscript data
16534
wenzelm
parents: 16486
diff changeset
  1234
     | "badcmd"         => isarscript data
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1235
     (* improperproofcmd: improper commands which *do not* belong in script *)
15401
ba28d103bada Support PGIP <whitespace>, <dostep>, <doitem> elements as input
aspinall
parents: 15400
diff changeset
  1236
     | "dostep"         => isarscript data
15286
b084384960d1 Add <undoitem> for theory-state undos.
aspinall
parents: 15268
diff changeset
  1237
     | "undostep"       => isarcmd "undos_proof 1"
15626
a8f718939500 Support new PGIP commands redostep, redoitem
aspinall
parents: 15570
diff changeset
  1238
     | "redostep"       => isarcmd "redo"
16534
wenzelm
parents: 16486
diff changeset
  1239
     | "abortgoal"      => isarcmd "ProofGeneral.kill_proof"
wenzelm
parents: 16486
diff changeset
  1240
     | "forget"         => error "Not implemented"
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1241
     | "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
  1242
     (* 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
  1243
     | "askids"         => askids (thyname_attro attrs, objtype_attro attrs)
16534
wenzelm
parents: 16486
diff changeset
  1244
     | "showid"         => showid (thyname_attro attrs, objtype_attr attrs, name_attr attrs)
wenzelm
parents: 16486
diff changeset
  1245
     | "askguise"       => send_informguise (!currently_open_file,
wenzelm
parents: 16486
diff changeset
  1246
                                             SOME (topthy_name()) handle Toplevel.UNDEF => NONE,
wenzelm
parents: 16486
diff changeset
  1247
                                             topproofpos())
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
  1248
     | "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
  1249
     | "showproofstate" => isarcmd "pr"
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1250
     | "showctxt"       => isarcmd "print_theory"   (* more useful than print_context *)
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1251
     | "searchtheorems" => isarcmd ("thms_containing " ^ xmltext data)
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1252
     | "setlinewidth"   => isarcmd ("pretty_setmargin " ^ xmltext data)
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1253
     | "viewdoc"        => isarcmd ("print_" ^ xmltext data) (* FIXME: isatool doc? *)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1254
     (* properfilecmd: proper theory-level script commands *)
15401
ba28d103bada Support PGIP <whitespace>, <dostep>, <doitem> elements as input
aspinall
parents: 15400
diff changeset
  1255
     (* FIXME: next three are sent by Eclipse, can be removed in favour of doitem *)
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1256
     | "opentheory"     => isarscript data
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1257
     | "theoryitem"     => isarscript data
16534
wenzelm
parents: 16486
diff changeset
  1258
     | "closetheory"    => let
wenzelm
parents: 16486
diff changeset
  1259
                              val thyname = topthy_name()
wenzelm
parents: 16486
diff changeset
  1260
                           in (isarscript data;
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1261
                               writeln ("Theory " ^ quote thyname ^ " completed."))
16534
wenzelm
parents: 16486
diff changeset
  1262
                           end
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1263
     (* improperfilecmd: theory-level commands not in script *)
15401
ba28d103bada Support PGIP <whitespace>, <dostep>, <doitem> elements as input
aspinall
parents: 15400
diff changeset
  1264
     | "doitem"         => isarscript data
15286
b084384960d1 Add <undoitem> for theory-state undos.
aspinall
parents: 15268
diff changeset
  1265
     | "undoitem"       => isarcmd "ProofGeneral.undo"
15626
a8f718939500 Support new PGIP commands redostep, redoitem
aspinall
parents: 15570
diff changeset
  1266
     | "redoitem"       => isarcmd "ProofGeneral.redo"
15145
07360eef9f4f Version for PGIP 2.X, with greatly improved parsing and XML handling.
aspinall
parents: 15134
diff changeset
  1267
     | "aborttheory"    => isarcmd ("init_toplevel")
17217
954c0f265203 added PGASCII print_mode, which represents special chars as ASCII 1 + A ... Z;
wenzelm
parents: 17057
diff changeset
  1268
     | "retracttheory"  => isarcmd ("kill_thy " ^ quote (thyname_attr attrs))
15173