src/Pure/ProofGeneral/parsing.ML
author wenzelm
Fri, 19 Jan 2007 22:08:08 +0100
changeset 22101 6d13239d5f52
parent 21971 513e1d82640d
child 22160 27cdecde8c2b
permissions -rw-r--r--
moved parts of OuterParse to SpecParse;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     1
(*  Title:      Pure/ProofGeneral/parsing.ML
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     2
    ID:         $Id$
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     3
    Author:     David Aspinall
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     4
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
     5
Parsing Isabelle theory files to add PGIP markup.
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     6
*)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     7
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     8
signature PGIP_PARSER =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
     9
sig
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
    10
    val pgip_parser: PgipMarkup.pgip_parser
21971
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
    11
    val init : unit -> unit		     (* clear state *)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    12
end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    13
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    14
structure PgipParser : PGIP_PARSER =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    15
struct
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    16
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    17
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    18
(** Parsing proof scripts without execution **)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    19
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    20
structure P = OuterParse;
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    21
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
    22
structure D = PgipMarkup;
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
    23
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    24
(* Notes.
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    25
   This is quite tricky, because 1) we need to put back whitespace which
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    26
   was removed during parsing so we can provide markup around commands;
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    27
   2) parsing is intertwined with execution in Isar so we have to repeat
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    28
   the parsing to extract interesting parts of commands.  The trace of
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    29
   tokens parsed which is now recorded in each transition (added by
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    30
   Markus June '04) helps do this, but the mechanism is still a bad mess.
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    31
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    32
   If we had proper parse trees it would be easy, although having a
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
    33
   fixed type of trees might be hard with Isar's extensible parser.
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    34
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    35
   Probably the best solution is to produce the meta-information at
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    36
   the same time as the parse, for each command, e.g. by recording a
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    37
   list of (name,objtype) pairs which record the bindings created by
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    38
   a command.  This would require changing the interfaces in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    39
   outer_syntax.ML (or providing new ones),
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    40
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    41
    datatype metainfo = Binding of string * string  (* name, objtype *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    42
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    43
    val command_withmetainfo: string -> string -> string ->
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    44
      (token list ->
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    45
       ((Toplevel.transition -> Toplevel.transition) * metainfo list) *
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    46
       token list) -> parser
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    47
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    48
   We'd also like to render terms as they appear in output, but this
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    49
   will be difficult because inner syntax is extensible and we don't
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    50
   have the correct syntax to hand when just doing outer parsing
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    51
   without execution.  A reasonable approximation could
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    52
   perhaps be obtained by using the syntax of the current context.
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    53
   However, this would mean more mess trying to pick out terms,
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    54
   so at this stage a more serious change to the Isar functions
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    55
   seems necessary.
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    56
*)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    57
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    58
local
21971
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
    59
    val keywords_classification_table = ref (NONE: string Symtab.table option)
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
    60
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
    61
in
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
    62
    fun get_keywords_classification_table () =
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
    63
        case (!keywords_classification_table) of
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
    64
          SOME t => t
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
    65
        | NONE => (let
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
    66
                     val tab = fold (fn (c, _, k, _) => Symtab.update (c, k))
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
    67
                                    (OuterSyntax.dest_parsers ()) Symtab.empty;
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
    68
                   in (keywords_classification_table := SOME tab; tab) end)
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
    69
  
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
    70
    (* To allow dynamic extensions to language during interactive use
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
    71
       we need a hook in outer_syntax.ML to reset our table.  But this is
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
    72
       pretty obscure; initialisation at startup should suffice. *)
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
    73
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
    74
    fun init () = (keywords_classification_table := NONE)
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
    75
end
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
    76
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
    77
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
    78
local
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    79
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
    80
    fun whitespace str = D.Whitespace { text=str }
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    81
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    82
    (* an extra token is needed to terminate the command *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    83
    val sync = OuterSyntax.scan "\\<^sync>";
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    84
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
    85
    fun nameparse elt objtyp nameP toks = 
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
    86
        (fst (nameP (toks@sync)))
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
    87
        handle _ => (error ("Error occurred in name parser for " ^ elt ^
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
    88
                            "(objtype: " ^ objtyp ^ ")");
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
    89
                     "")
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    90
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    91
    fun parse_warning msg = warning ("script->PGIP markup parser: " ^ msg)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    92
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    93
    fun xmls_of_thy_begin (name,toks,str) = (* see isar_syn.ML/theoryP *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    94
        let
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    95
            val ((thyname,imports,files),_) = ThyHeader.args (toks@sync)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
    96
        in
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
    97
            [D.Opentheory { thyname=thyname, 
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
    98
			    parentnames = imports,
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
    99
			    text = str }]
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   100
        end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   101
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   102
    fun xmls_of_thy_decl (name,toks,str) = (* see isar_syn.ML/thy_decl cases  *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   103
        let
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   104
            (* NB: PGIP only deals with single name bindings at the moment;
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   105
               potentially we could markup grouped definitions several times but
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   106
               that might suggest the wrong structure to the editor?
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   107
               Better alternative would be to put naming closer around text,
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   108
               but to do that we'd be much better off modifying the real parser
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   109
               instead of reconstructing it here. *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   110
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   111
            val plain_items = (* no names, unimportant names, or too difficult *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   112
                ["defaultsort","arities","judgement","finalconsts",
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   113
                 "syntax", "nonterminals", "translations",
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   114
                 "global", "local", "hide",
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   115
                 "ML_setup", "setup", "method_setup",
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   116
                 "parse_ast_translation", "parse_translation", "print_translation",
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   117
                 "typed_print_translation", "print_ast_translation", "token_translation",
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   118
                 "oracle",
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   119
                 "declare"]
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   120
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   121
            fun named_item nameP ty = 
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   122
		[D.Theoryitem {text=str,name=SOME (nameparse "theoryitem" ty nameP toks),objtype=SOME ty}]
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   123
	    val plain_item = 
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   124
		[D.Theoryitem {text=str,name=NONE,objtype=NONE}]
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   125
	    val doccomment = 
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   126
		[D.Doccomment {text=str}]
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   127
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   128
            val opt_overloaded = P.opt_keyword "overloaded";
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   129
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   130
            val thmnameP = (* see isar_syn.ML/theoremsP *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   131
                let
22101
6d13239d5f52 moved parts of OuterParse to SpecParse;
wenzelm
parents: 21971
diff changeset
   132
                    val name_facts = P.and_list1 ((SpecParse.opt_thm_name "=" --| SpecParse.xthms1) >> #1)
6d13239d5f52 moved parts of OuterParse to SpecParse;
wenzelm
parents: 21971
diff changeset
   133
                    val theoremsP = P.opt_target |-- name_facts >> (fn [] => "" | x::_ => x)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   134
                in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   135
                    theoremsP
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   136
                end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   137
        in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   138
            (* TODO: ideally we would like to render terms properly, just as they are
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   139
               in output. This implies using PGML for symbols and variables/atoms.
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   140
               BUT it's rather tricky without having the correct concrete syntax to hand,
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   141
               and even if we did, we'd have to mess around here a whole lot more first
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   142
               to pick out the terms from the syntax. *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   143
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   144
            if member (op =) plain_items name then plain_item
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   145
            else case name of
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   146
                     "text"      => doccomment
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   147
                   | "text_raw"  => doccomment
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   148
                   | "typedecl"  => named_item (P.type_args |-- P.name) "type"
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   149
                   | "types"     => named_item (P.type_args |-- P.name) "type"
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   150
                   | "classes"   => named_item P.name "class"
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   151
                   | "classrel"  => named_item P.name "class"
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   152
                   | "consts"    => named_item (P.const >> #1) "term"
22101
6d13239d5f52 moved parts of OuterParse to SpecParse;
wenzelm
parents: 21971
diff changeset
   153
                   | "axioms"    => named_item (SpecParse.spec_name >> (#1 o #1)) "theorem"
6d13239d5f52 moved parts of OuterParse to SpecParse;
wenzelm
parents: 21971
diff changeset
   154
                   | "defs"      => named_item (opt_overloaded |-- SpecParse.spec_name >> (#1 o #1)) "theorem"
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   155
                   | "constdefs" => named_item P.name (* FIXME: heavily simplified/wrong *) "term"
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   156
                   | "theorems"  => named_item thmnameP "thmset"
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   157
                   | "lemmas"    => named_item thmnameP "thmset"
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   158
                   | "oracle"    => named_item P.name "oracle"
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   159
                   | "locale"    => named_item ((P.opt_keyword "open" >> not) |-- P.name) "locale"
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   160
                   | _ => (parse_warning ("Unrecognized thy-decl command: " ^ name); 
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   161
			   plain_item)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   162
        end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   163
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   164
    fun xmls_of_thy_goal (name,toks,str) =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   165
        let
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   166
            (* see isar_syn.ML/gen_theorem *)
22101
6d13239d5f52 moved parts of OuterParse to SpecParse;
wenzelm
parents: 21971
diff changeset
   167
         val statement = P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.propp);
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   168
         val general_statement =
22101
6d13239d5f52 moved parts of OuterParse to SpecParse;
wenzelm
parents: 21971
diff changeset
   169
            statement >> pair [] || Scan.repeat SpecParse.locale_element -- (P.$$$ "shows" |-- statement);
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   170
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   171
            val gen_theoremP =
22101
6d13239d5f52 moved parts of OuterParse to SpecParse;
wenzelm
parents: 21971
diff changeset
   172
                P.opt_target -- Scan.optional (SpecParse.opt_thm_name ":" --|
6d13239d5f52 moved parts of OuterParse to SpecParse;
wenzelm
parents: 21971
diff changeset
   173
                 Scan.ahead (SpecParse.locale_keyword || P.$$$ "shows")) ("", []) --
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   174
                                 general_statement >> (fn ((locale, a), (elems, concl)) =>
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   175
                                                         fst a) (* a : (bstring * Args.src list) *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   176
22101
6d13239d5f52 moved parts of OuterParse to SpecParse;
wenzelm
parents: 21971
diff changeset
   177
            val nameP = P.opt_target |-- (Scan.optional ((SpecParse.opt_thm_name ":") >> #1) "")
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   178
	    val thmname = nameparse "opengoal" "theorem" nameP toks
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   179
        in
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   180
            [D.Opengoal {thmname=SOME thmname, text=str},
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   181
             D.Openblock {metavarid=NONE,name=NONE,objtype=SOME "theorem-proof"}]
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   182
        end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   183
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   184
    fun xmls_of_qed (name,str) =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   185
        let val qedmarkup  =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   186
                (case name of
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   187
                     "sorry" => D.Postponegoal {text=str}
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   188
                   | "oops"  => D.Giveupgoal {text=str}
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   189
                   | "done"  => D.Closegoal {text=str}
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   190
                   | "by"    => D.Closegoal {text=str}  (* nested or toplevel *)
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   191
                   | "qed"   => D.Closegoal {text=str}  (* nested or toplevel *)
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   192
                   | "."     => D.Closegoal {text=str}  (* nested or toplevel *)
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   193
                   | ".."    => D.Closegoal {text=str}  (* nested or toplevel *)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   194
                   | other => (* default to closegoal: may be wrong for extns *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   195
                                  (parse_warning
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   196
                                       ("Unrecognized qed command: " ^ quote other);
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   197
                                       D.Closegoal {text=str}))
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   198
        in qedmarkup :: [D.Closeblock {}] end
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   199
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   200
    fun xmls_of_kind kind (name,toks,str) =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   201
    case kind of
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   202
      "control"        => [D.Badcmd {text=str}]
21971
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
   203
    | "diag"           => [D.Spuriouscmd {text=str}]
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   204
    (* theory/files *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   205
    | "theory-begin"   => xmls_of_thy_begin (name,toks,str)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   206
    | "theory-decl"    => xmls_of_thy_decl (name,toks,str)
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   207
    | "theory-heading" => [D.Doccomment {text=str}]
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   208
    | "theory-script"  => [D.Theoryitem {name=NONE,objtype=NONE,text=str}]
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   209
    | "theory-end"     => [D.Closetheory {text=str}]
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   210
    (* proof control *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   211
    | "theory-goal"    => xmls_of_thy_goal (name,toks,str)
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   212
    | "proof-heading"  => [D.Doccomment {text=str}]
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   213
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   214
    | "proof-goal"     => (* nested proof: have, show, ... *)
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   215
      [D.Opengoal {text=str,thmname=NONE}, 
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   216
       D.Openblock {metavarid=NONE,name=NONE,objtype=NONE}]
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   217
			  
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   218
    | "proof-block"    => [D.Proofstep {text=str}]
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   219
    | "proof-open"     => [D.Openblock {metavarid=NONE,name=NONE,objtype=NONE}, 
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   220
			   D.Proofstep {text=str} ]
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   221
    | "proof-close"    => [D.Proofstep {text=str}, D.Closeblock {}]
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   222
    | "proof-script"   => [D.Proofstep {text=str}]
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   223
    | "proof-chain"    => [D.Proofstep {text=str}]
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   224
    | "proof-decl"     => [D.Proofstep {text=str}]
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   225
    | "proof-asm"      => [D.Proofstep {text=str}]
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   226
    | "proof-asm-goal" => (* nested proof: obtain, ... *)
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   227
      [D.Opengoal {text=str,thmname=NONE}, 
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   228
       D.Openblock {metavarid=NONE,name=NONE,objtype=NONE}]
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   229
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   230
    | "qed"            => xmls_of_qed (name,str)
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   231
    | "qed-block"      => xmls_of_qed (name,str)
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   232
    | "qed-global"     => xmls_of_qed (name,str)
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   233
    | other => (* default for anything else is "spuriouscmd", ***ignored for undo*** *)
21971
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
   234
      (parse_warning ("Internal inconsistency, unrecognized keyword kind: " ^ quote other ^
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
   235
		      "(treated as spuriouscmd)");
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   236
       [D.Spuriouscmd {text=str}])
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   237
in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   238
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   239
fun xmls_of_transition (name,str,toks) =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   240
   let
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   241
     val classification = Symtab.lookup (get_keywords_classification_table ()) name
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   242
   in case classification of
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   243
          SOME k => (xmls_of_kind k (name,toks,str))
21971
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
   244
        | NONE => (* an uncategorized keyword is treated as a theory item (maybe wrong) *)
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
   245
          (parse_warning ("Uncategorized command found: " ^ name ^ " -- using theoryitem");
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
   246
           [D.Theoryitem {name=NONE,objtype=NONE,text=str}])
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   247
   end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   248
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   249
fun markup_comment_whs [] = []
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   250
  | markup_comment_whs (toks as t::ts) = (* this would be a lot neater if we could match on toks! *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   251
    let
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   252
        val (prewhs,rest) = take_prefix (OuterLex.is_kind OuterLex.Space) toks
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   253
    in
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   254
        if not (null prewhs) then
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   255
            D.Whitespace {text=implode (map OuterLex.unparse prewhs)}
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   256
            :: (markup_comment_whs rest)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   257
        else
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   258
            D.Comment {text=OuterLex.unparse t} ::
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   259
            (markup_comment_whs ts)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   260
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   261
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   262
fun xmls_pre_cmd [] = ([],[])
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   263
  | xmls_pre_cmd toks =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   264
    let
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   265
        (* an extra token is needed to terminate the command *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   266
        val sync = OuterSyntax.scan "\\<^sync>";
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   267
        val spaceP = Scan.bulk (Scan.one (fn t =>not (OuterLex.is_proper t)) >> OuterLex.val_of) >> implode
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   268
        val text_with_whs =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   269
            ((spaceP || Scan.succeed "") --
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   270
             (P.short_ident || P.long_ident || P.sym_ident || P.string || P.number || P.verbatim) >> op^)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   271
             -- (spaceP || Scan.succeed "") >> op^
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   272
        val (prewhs,rest1) = take_prefix (not o OuterLex.is_proper) (toks@sync)
21971
513e1d82640d Fix diagnostic kind (*are* spuriouscmd). Add init to get right table for logic at startup. Use theoryitem as default for unrecognised command.
aspinall
parents: 21966
diff changeset
   273
        (* NB: this collapses  doccomment,(doccomment|whitespace)* to a single doccomment *)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   274
        val (_,rest2) = (Scan.bulk (P.$$$ "--" |-- text_with_whs) >> implode || Scan.succeed "") rest1
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   275
        val (postwhs,rest3) = take_prefix (not o OuterLex.is_proper) rest2
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   276
    in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   277
        ((markup_comment_whs prewhs) @
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   278
         (if (length rest2 = length rest1)  then []
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   279
          else 
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   280
	      [D.Doccomment 
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   281
		   {text= implode
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   282
                          (map OuterLex.unparse (Library.take (length rest1 - length rest2, rest1)))}]
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   283
              @
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   284
              (markup_comment_whs postwhs)),
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   285
              Library.take (length rest3 - 1,rest3))
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   286
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   287
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   288
fun xmls_of_impropers toks =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   289
    let
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   290
        val (xmls,rest) = xmls_pre_cmd toks
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   291
	val unparsed =  
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   292
	    case rest of [] => []
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   293
		       | _ => [D.Unparseable 
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   294
			      {text= implode (map OuterLex.unparse rest)}]
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   295
    in
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   296
        xmls @ unparsed
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   297
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   298
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   299
end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   300
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   301
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   302
local
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   303
    (* we have to weave together the whitespace/comments with proper tokens
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   304
       to reconstruct the input. *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   305
    (* TODO: see if duplicating isar_output/parse_thy can help here *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   306
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   307
    fun match_tokens ([],us,vs) = (rev vs,us)  (* used, unused *)
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   308
      | match_tokens (t::ts, w::ws, vs) =
21966
edab0ecfbd7c removed misleading OuterLex.eq_token;
wenzelm
parents: 21902
diff changeset
   309
        if (t: OuterLex.token) = w  (* FIXME !? *)
21902
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   310
          then match_tokens (ts, ws, w::vs)
8e5e2571c716 made SML/NJ happy
haftmann
parents: 21867
diff changeset
   311
          else match_tokens (t::ts, ws, w::vs)
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   312
      | match_tokens _ = error ("match_tokens: mismatched input parse")
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   313
in
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   314
    fun pgip_parser str =
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   315
    let
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   316
       (* parsing:   See outer_syntax.ML/toplevel_source *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   317
       fun parse_loop ([],[],xmls) = xmls
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   318
         | parse_loop ([],itoks,xmls) = xmls @ (xmls_of_impropers itoks)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   319
         | parse_loop ((nm,toks,_)::trs,itoks,xmls) =
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   320
           let
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   321
               (* first proper token after whitespace/litcomment/whitespace is command *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   322
               val (xmls_pre_cmd,cmditoks') = xmls_pre_cmd itoks
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   323
               val (cmdtok,itoks') = case cmditoks' of x::xs => (x,xs)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   324
                                                     | _ => error("proof_general/parse_loop impossible")
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   325
               val (utoks,itoks'') = match_tokens (toks,itoks',[])
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   326
               (* FIXME: should take trailing [w/s+] semicolon too in utoks *)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   327
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   328
               val str = implode (map OuterLex.unparse (cmdtok::utoks))
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   329
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   330
               val xmls_tr  = xmls_of_transition (nm,str,toks)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   331
           in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   332
               parse_loop(trs,itoks'',xmls @ xmls_pre_cmd @ xmls_tr)
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   333
           end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   334
    in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   335
        (let val toks = OuterSyntax.scan str
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   336
         in
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   337
             parse_loop (OuterSyntax.read toks, toks, [])
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   338
         end)
21867
8750fbc28d5c Add abstraction for objtypes and documents.
aspinall
parents: 21655
diff changeset
   339
           handle _ => [D.Unparseable {text=str}]
21637
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   340
    end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   341
end
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   342
a7b156c404e2 Revamped Proof General interface.
aspinall
parents:
diff changeset
   343
end