removed obsolete ProofGeneral/parsing.ML;
authorwenzelm
Sun Nov 04 17:12:14 2007 +0100 (2007-11-04)
changeset 2527576d7f3fd4fb3
parent 25274 5c590f3f7a09
child 25276 f9237f6f3a8d
removed obsolete ProofGeneral/parsing.ML;
src/Pure/IsaMakefile
src/Pure/ProofGeneral/ROOT.ML
src/Pure/ProofGeneral/parsing.ML
src/Pure/ProofGeneral/pgip_tests.ML
src/Pure/ProofGeneral/proof_general_pgip.ML
     1.1 --- a/src/Pure/IsaMakefile	Sun Nov 04 16:43:31 2007 +0100
     1.2 +++ b/src/Pure/IsaMakefile	Sun Nov 04 17:12:14 2007 +0100
     1.3 @@ -54,26 +54,26 @@
     1.4    ML/ml_context.ML ML/ml_lex.ML ML/ml_parse.ML ML/ml_syntax.ML			\
     1.5    Proof/extraction.ML Proof/proof_rewrite_rules.ML Proof/proof_syntax.ML	\
     1.6    Proof/proofchecker.ML Proof/reconstruct.ML ProofGeneral/ROOT.ML		\
     1.7 -  ProofGeneral/parsing.ML ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML	\
     1.8 +  ProofGeneral/pgip.ML ProofGeneral/pgip_input.ML				\
     1.9    ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML			\
    1.10    ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML			\
    1.11 -  ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML ProofGeneral/pgml_isabelle.ML				\
    1.12 -  ProofGeneral/preferences.ML ProofGeneral/proof_general_emacs.ML 		\
    1.13 -  ProofGeneral/proof_general_pgip.ML Pure.thy ROOT.ML Syntax/ast.ML		\
    1.14 -  Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML Syntax/printer.ML		\
    1.15 -  Syntax/simple_syntax.ML Syntax/syn_ext.ML Syntax/syn_trans.ML Syntax/syntax.ML\
    1.16 -  Syntax/type_ext.ML Thy/html.ML Thy/latex.ML Thy/present.ML			\
    1.17 -  Thy/term_style.ML Thy/thm_database.ML Thy/thm_deps.ML Thy/thy_edit.ML		\
    1.18 -  Thy/thy_header.ML Thy/thy_info.ML Thy/thy_load.ML Thy/thy_output.ML		\
    1.19 -  Tools/ROOT.ML Tools/invoke.ML Tools/named_thms.ML Tools/xml_syntax.ML		\
    1.20 -  assumption.ML axclass.ML codegen.ML compress.ML config.ML			\
    1.21 -  conjunction.ML consts.ML context.ML context_position.ML conv.ML		\
    1.22 -  defs.ML display.ML drule.ML envir.ML fact_index.ML goal.ML interpretation.ML  \
    1.23 -  library.ML logic.ML meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML	\
    1.24 -  old_goals.ML pattern.ML primitive_defs.ML proofterm.ML pure_setup.ML		\
    1.25 -  pure_thy.ML search.ML sign.ML simplifier.ML sorts.ML subgoal.ML		\
    1.26 -  tactic.ML tctical.ML term.ML term_subst.ML theory.ML thm.ML type.ML		\
    1.27 -  type_infer.ML unify.ML variable.ML
    1.28 +  ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML				\
    1.29 +  ProofGeneral/pgml_isabelle.ML ProofGeneral/preferences.ML			\
    1.30 +  ProofGeneral/proof_general_emacs.ML ProofGeneral/proof_general_pgip.ML	\
    1.31 +  Pure.thy ROOT.ML Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML		\
    1.32 +  Syntax/parser.ML Syntax/printer.ML Syntax/simple_syntax.ML Syntax/syn_ext.ML	\
    1.33 +  Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML		\
    1.34 +  Thy/latex.ML Thy/present.ML Thy/term_style.ML Thy/thm_database.ML		\
    1.35 +  Thy/thm_deps.ML Thy/thy_edit.ML Thy/thy_header.ML Thy/thy_info.ML		\
    1.36 +  Thy/thy_load.ML Thy/thy_output.ML Tools/ROOT.ML Tools/invoke.ML		\
    1.37 +  Tools/named_thms.ML Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML	\
    1.38 +  compress.ML config.ML conjunction.ML consts.ML context.ML context_position.ML	\
    1.39 +  conv.ML defs.ML display.ML drule.ML envir.ML fact_index.ML goal.ML		\
    1.40 +  interpretation.ML library.ML logic.ML meta_simplifier.ML more_thm.ML 		\
    1.41 +  morphism.ML name.ML net.ML old_goals.ML pattern.ML primitive_defs.ML		\
    1.42 +  proofterm.ML pure_setup.ML pure_thy.ML search.ML sign.ML simplifier.ML	\
    1.43 +  sorts.ML subgoal.ML tactic.ML tctical.ML term.ML term_subst.ML theory.ML	\
    1.44 +  thm.ML type.ML type_infer.ML unify.ML variable.ML
    1.45  	@./mk
    1.46  
    1.47  
     2.1 --- a/src/Pure/ProofGeneral/ROOT.ML	Sun Nov 04 16:43:31 2007 +0100
     2.2 +++ b/src/Pure/ProofGeneral/ROOT.ML	Sun Nov 04 17:12:14 2007 +0100
     2.3 @@ -18,8 +18,6 @@
     2.4  (use |> setmp Proofterm.proofs 1 |> setmp quick_and_dirty true) "preferences.ML";
     2.5  use "pgip_parser.ML";
     2.6  
     2.7 -use "parsing.ML";   (* old version *)
     2.8 -
     2.9  use "pgip_tests.ML";
    2.10  
    2.11  use "proof_general_pgip.ML";
     3.1 --- a/src/Pure/ProofGeneral/parsing.ML	Sun Nov 04 16:43:31 2007 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,348 +0,0 @@
     3.4 -(*  Title:      Pure/ProofGeneral/parsing.ML
     3.5 -    ID:         $Id$
     3.6 -    Author:     David Aspinall
     3.7 -
     3.8 -Parsing Isabelle theory files to add PGIP markup -- OLD VERSION.
     3.9 -*)
    3.10 -
    3.11 -signature OLD_PGIP_PARSER =
    3.12 -sig
    3.13 -    val pgip_parser: PgipMarkup.pgip_parser
    3.14 -    val init : unit -> unit		     (* clear state *)
    3.15 -end
    3.16 -
    3.17 -structure OldPgipParser : OLD_PGIP_PARSER =
    3.18 -struct
    3.19 -
    3.20 -
    3.21 -(** Parsing proof scripts without execution **)
    3.22 -
    3.23 -structure P = OuterParse;
    3.24 -
    3.25 -structure D = PgipMarkup;
    3.26 -structure I = PgipIsabelle;
    3.27 -structure T = PgipTypes;
    3.28 -
    3.29 -(* Notes.
    3.30 -   This is quite tricky, because 1) we need to put back whitespace which
    3.31 -   was removed during parsing so we can provide markup around commands;
    3.32 -   2) parsing is intertwined with execution in Isar so we have to repeat
    3.33 -   the parsing to extract interesting parts of commands.  The trace of
    3.34 -   tokens parsed which is now recorded in each transition (added by
    3.35 -   Markus June '04) helps do this, but the mechanism is still a bad mess.
    3.36 -
    3.37 -   If we had proper parse trees it would be easy, although having a
    3.38 -   fixed type of trees might be hard with Isar's extensible parser.
    3.39 -
    3.40 -   Probably the best solution is to produce the meta-information at
    3.41 -   the same time as the parse, for each command, e.g. by recording a
    3.42 -   list of (name,objtype) pairs which record the bindings created by
    3.43 -   a command.  This would require changing the interfaces in
    3.44 -   outer_syntax.ML (or providing new ones),
    3.45 -
    3.46 -    datatype metainfo = Binding of string * string  (* name, objtype *)
    3.47 -
    3.48 -    val command_withmetainfo: string -> string -> string ->
    3.49 -      (token list ->
    3.50 -       ((Toplevel.transition -> Toplevel.transition) * metainfo list) *
    3.51 -       token list) -> parser
    3.52 -
    3.53 -   We'd also like to render terms as they appear in output, but this
    3.54 -   will be difficult because inner syntax is extensible and we don't
    3.55 -   have the correct syntax to hand when just doing outer parsing
    3.56 -   without execution.  A reasonable approximation could
    3.57 -   perhaps be obtained by using the syntax of the current context.
    3.58 -   However, this would mean more mess trying to pick out terms,
    3.59 -   so at this stage a more serious change to the Isar functions
    3.60 -   seems necessary.
    3.61 -*)
    3.62 -
    3.63 -local
    3.64 -    val keywords_classification_table = ref (NONE: string Symtab.table option)
    3.65 -
    3.66 -in
    3.67 -    fun get_keywords_classification_table () =
    3.68 -        case (!keywords_classification_table) of
    3.69 -          SOME t => t
    3.70 -        | NONE => (let
    3.71 -                     val tab = fold (fn (c, _, k, _) => Symtab.update (c, k))
    3.72 -                                    (OuterSyntax.dest_parsers ()) Symtab.empty;
    3.73 -                   in (keywords_classification_table := SOME tab; tab) end)
    3.74 -  
    3.75 -    (* To allow dynamic extensions to language during interactive use
    3.76 -       we need a hook in outer_syntax.ML to reset our table.  But this is
    3.77 -       pretty obscure; initialisation at startup should suffice. *)
    3.78 -
    3.79 -    fun init () = (keywords_classification_table := NONE)
    3.80 -end
    3.81 -
    3.82 -
    3.83 -local
    3.84 -
    3.85 -    fun whitespace str = D.Whitespace { text=str }
    3.86 -
    3.87 -    (* an extra token is needed to terminate the command *)
    3.88 -    val sync = OuterSyntax.scan "\\<^sync>";
    3.89 -
    3.90 -    fun nameparse elt objtyp nameP toks = 
    3.91 -        (fst (nameP (toks@sync)))
    3.92 -        handle _ => (error ("Error occurred in name parser for " ^ elt ^
    3.93 -                            "(objtype: " ^ (T.name_of_objtype objtyp) ^ ")");
    3.94 -                     "")
    3.95 -
    3.96 -    fun parse_warning msg = warning ("script->PGIP markup parser: " ^ msg)
    3.97 -
    3.98 -    fun xmls_of_thy_begin (name,toks,str) = (* see isar_syn.ML/theoryP *)
    3.99 -        let
   3.100 -            val ((thyname,imports,files),_) = ThyHeader.args (toks@sync)
   3.101 -        in
   3.102 -            [D.Opentheory { thyname=SOME thyname, 
   3.103 -			    parentnames = imports,
   3.104 -			    text = str },
   3.105 -	     D.Openblock { metavarid=NONE,name=NONE,objtype=SOME I.ObjTheoryBody }]
   3.106 -        end
   3.107 -
   3.108 -    fun xmls_of_thy_decl (name,toks,str) = (* see isar_syn.ML/thy_decl cases  *)
   3.109 -        let
   3.110 -            (* NB: PGIP only deals with single name bindings at the moment;
   3.111 -               potentially we could markup grouped definitions several times but
   3.112 -               that might suggest the wrong structure to the editor?
   3.113 -               Better alternative would be to put naming closer around text,
   3.114 -               but to do that we'd be much better off modifying the real parser
   3.115 -               instead of reconstructing it here. *)
   3.116 -
   3.117 -            val plain_items = (* no names, unimportant names, or too difficult *)
   3.118 -                ["defaultsort","arities","judgement","finalconsts",
   3.119 -                 "syntax", "nonterminals", "translations",
   3.120 -                 "global", "local", "hide",
   3.121 -                 "ML_setup", "setup", "method_setup",
   3.122 -                 "parse_ast_translation", "parse_translation", "print_translation",
   3.123 -                 "typed_print_translation", "print_ast_translation", "token_translation",
   3.124 -                 "oracle",
   3.125 -                 "declare"]
   3.126 -
   3.127 -            fun named_item nameP ty = 
   3.128 -		[D.Theoryitem {text=str,
   3.129 -			       name=SOME (nameparse "theoryitem" ty nameP toks),
   3.130 -			       objtype=SOME ty}]
   3.131 -            val opt_overloaded = P.opt_keyword "overloaded";
   3.132 -
   3.133 -            val thmnameP = (* see isar_syn.ML/theoremsP *)
   3.134 -                let
   3.135 -                    val name_facts = P.and_list1 ((SpecParse.opt_thm_name "=" --| SpecParse.xthms1) >> #1)
   3.136 -                    val theoremsP = P.opt_target |-- name_facts >> (fn [] => "" | x::_ => x)
   3.137 -                in
   3.138 -                    theoremsP
   3.139 -                end
   3.140 -        in
   3.141 -            (* TODO: ideally we would like to render terms properly, just as they are
   3.142 -               in output. This implies using PGML for symbols and variables/atoms.
   3.143 -               BUT it's rather tricky without having the correct concrete syntax to hand,
   3.144 -               and even if we did, we'd have to mess around here a whole lot more first
   3.145 -               to pick out the terms from the syntax. *)
   3.146 -
   3.147 -            if member (op =) plain_items name then 
   3.148 -		[D.Theoryitem {text=str,name=NONE,objtype=NONE}]
   3.149 -            else case name of
   3.150 -                     "text"      => [D.Doccomment {text=str}]
   3.151 -                   | "text_raw"  => [D.Doccomment {text=str}]
   3.152 -                   | "typedecl"  => named_item (P.type_args |-- P.name) T.ObjType
   3.153 -                   | "types"     => named_item (P.type_args |-- P.name) T.ObjType
   3.154 -                   | "classes"   => named_item P.name I.ObjClass
   3.155 -                   | "classrel"  => named_item P.name I.ObjClass
   3.156 -                   | "consts"    => named_item (P.const >> #1) T.ObjTerm
   3.157 -                   | "axioms"    => named_item (SpecParse.spec_name >> (#1 o #1)) T.ObjTheorem
   3.158 -                   | "defs"      => named_item (opt_overloaded |-- SpecParse.spec_name >> (#1 o #1)) T.ObjTheorem
   3.159 -                   | "constdefs" => named_item P.name (* FIXME: heavily simplified/wrong *) T.ObjTerm
   3.160 -                   | "theorems"  => named_item thmnameP I.ObjTheoremSet
   3.161 -                   | "lemmas"    => named_item thmnameP I.ObjTheoremSet
   3.162 -                   | "oracle"    => named_item P.name I.ObjOracle
   3.163 -		   (* FIXME: locale needs to introduce a block *)
   3.164 -                   | "locale"    => named_item ((P.opt_keyword "open" >> not) |-- P.name) I.ObjLocale
   3.165 -                   | _ => (parse_warning ("Unrecognized thy-decl command: " ^ name); 
   3.166 -			   [D.Theoryitem {text=str,name=NONE,objtype=NONE}])
   3.167 -        end
   3.168 -
   3.169 -    fun xmls_of_thy_goal (name,toks,str) =
   3.170 -        let
   3.171 -            (* see isar_syn.ML/gen_theorem *)
   3.172 -         val statement = P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.propp);
   3.173 -         val general_statement =
   3.174 -            statement >> pair [] || Scan.repeat SpecParse.locale_element -- (P.$$$ "shows" |-- statement);
   3.175 -
   3.176 -            val gen_theoremP =
   3.177 -                P.opt_target -- Scan.optional (SpecParse.opt_thm_name ":" --|
   3.178 -                 Scan.ahead (SpecParse.locale_keyword || P.$$$ "shows")) ("", []) --
   3.179 -                                 general_statement >> (fn ((locale, a), (elems, concl)) =>
   3.180 -                                                         fst a) (* a : (bstring * Args.src list) *)
   3.181 -
   3.182 -            val nameP = P.opt_target |-- (Scan.optional ((SpecParse.opt_thm_name ":") >> #1) "")
   3.183 -	    val thmname = nameparse "opengoal" T.ObjTheorem nameP toks
   3.184 -        in
   3.185 -            [D.Opengoal {thmname=SOME thmname, text=str},
   3.186 -             D.Openblock {metavarid=NONE,name=NONE,objtype=SOME I.ObjProofBody}]
   3.187 -        end
   3.188 -
   3.189 -    fun xmls_of_qed (name,str) =
   3.190 -        let val qedmarkup  =
   3.191 -                (case name of
   3.192 -                     "sorry" => D.Postponegoal {text=str}
   3.193 -                   | "oops"  => D.Giveupgoal {text=str}
   3.194 -                   | "done"  => D.Closegoal {text=str}
   3.195 -                   | "by"    => D.Closegoal {text=str}  (* nested or toplevel *)
   3.196 -                   | "qed"   => D.Closegoal {text=str}  (* nested or toplevel *)
   3.197 -                   | "."     => D.Closegoal {text=str}  (* nested or toplevel *)
   3.198 -                   | ".."    => D.Closegoal {text=str}  (* nested or toplevel *)
   3.199 -                   | other => (* default to closegoal: may be wrong for extns *)
   3.200 -                                  (parse_warning
   3.201 -                                       ("Unrecognized qed command: " ^ quote other);
   3.202 -                                       D.Closegoal {text=str}))
   3.203 -        in qedmarkup :: [D.Closeblock {}] end
   3.204 -
   3.205 -    fun xmls_of_kind kind (name,toks,str) =
   3.206 -    case kind of
   3.207 -      "control"        => [D.Badcmd {text=str}]
   3.208 -    | "diag"           => [D.Spuriouscmd {text=str}]
   3.209 -    (* theory/files *)
   3.210 -    | "theory-begin"   => xmls_of_thy_begin (name,toks,str)
   3.211 -    | "theory-decl"    => xmls_of_thy_decl (name,toks,str)
   3.212 -    | "theory-heading" => [D.Closeblock {},
   3.213 -			   D.Doccomment {text=str},
   3.214 -			   D.Openblock {metavarid=NONE,name=NONE,objtype=SOME I.ObjTheoryBody}]
   3.215 -    | "theory-script"  => [D.Theoryitem {name=NONE,objtype=SOME I.ObjTheoryDecl,text=str}]
   3.216 -    | "theory-end"     => [D.Closeblock {}, D.Closetheory {text=str}]
   3.217 -    (* proof control *)
   3.218 -    | "theory-goal"    => xmls_of_thy_goal (name,toks,str)
   3.219 -    | "proof-heading"  => [D.Doccomment {text=str}]
   3.220 -    | "proof-goal"     => [D.Opengoal {text=str,thmname=NONE}, 
   3.221 -			   D.Openblock {metavarid=NONE,name=NONE,objtype=SOME I.ObjProofBody}]
   3.222 -    | "proof-block"    => [D.Closeblock {}, 
   3.223 -			   D.Proofstep {text=str},
   3.224 -			   D.Openblock {metavarid=NONE,name=NONE,objtype=SOME I.ObjProofBody}]
   3.225 -    | "proof-open"     => [D.Openblock {metavarid=NONE,name=NONE,objtype=SOME I.ObjProofBody}, 
   3.226 -			   D.Proofstep {text=str} ]
   3.227 -    | "proof-close"    => [D.Proofstep {text=str}, D.Closeblock {}]
   3.228 -    | "proof-script"   => [D.Proofstep {text=str}]
   3.229 -    | "proof-chain"    => [D.Proofstep {text=str}]
   3.230 -    | "proof-decl"     => [D.Proofstep {text=str}]
   3.231 -    | "proof-asm"      => [D.Proofstep {text=str}]
   3.232 -    | "proof-asm-goal" => [D.Opengoal {text=str,thmname=NONE}, 
   3.233 -			   D.Openblock {metavarid=NONE,name=NONE,objtype=NONE}]
   3.234 -    | "qed"            => xmls_of_qed (name,str)
   3.235 -    | "qed-block"      => xmls_of_qed (name,str)
   3.236 -    | "qed-global"     => xmls_of_qed (name,str)
   3.237 -    | other => (* default for anything else is "spuriouscmd", ***ignored for undo*** *)
   3.238 -      (parse_warning ("Internal inconsistency, unrecognized keyword kind: " ^ quote other ^
   3.239 -		      "(treated as spuriouscmd)");
   3.240 -       [D.Spuriouscmd {text=str}])
   3.241 -in
   3.242 -
   3.243 -fun xmls_of_transition (name,str,toks) =
   3.244 -   let
   3.245 -     val classification = Symtab.lookup (get_keywords_classification_table ()) name
   3.246 -   in case classification of
   3.247 -          SOME k => (xmls_of_kind k (name,toks,str))
   3.248 -        | NONE => (* an uncategorized keyword is treated as a theory item (maybe wrong) *)
   3.249 -          (parse_warning ("Uncategorized command found: " ^ name ^ " -- using theoryitem");
   3.250 -           [D.Theoryitem {name=NONE,objtype=NONE,text=str}])
   3.251 -   end
   3.252 -
   3.253 -
   3.254 -(* this would be a lot neater if we could match on toks! *)
   3.255 -fun markup_comment_whs [] = []
   3.256 -  | markup_comment_whs (toks as t::ts) = 
   3.257 -    let
   3.258 -        val (prewhs,rest) = take_prefix (OuterLex.is_kind OuterLex.Space) toks
   3.259 -    in
   3.260 -        if not (null prewhs) then
   3.261 -            D.Whitespace {text=implode (map OuterLex.unparse prewhs)}
   3.262 -            :: (markup_comment_whs rest)
   3.263 -        else
   3.264 -            D.Comment {text=OuterLex.unparse t} ::
   3.265 -            (markup_comment_whs ts)
   3.266 -    end
   3.267 -
   3.268 -fun xmls_pre_cmd [] = ([],[])
   3.269 -  | xmls_pre_cmd toks =
   3.270 -    let
   3.271 -        (* an extra token is needed to terminate the command *)
   3.272 -        val sync = OuterSyntax.scan "\\<^sync>";
   3.273 -        val spaceP = Scan.bulk (Scan.one (fn t =>not (OuterLex.is_proper t)) >> OuterLex.val_of) >> implode
   3.274 -        val text_with_whs =
   3.275 -            ((spaceP || Scan.succeed "") --
   3.276 -             (P.short_ident || P.long_ident || P.sym_ident || P.string || P.number || P.verbatim) >> op^)
   3.277 -             -- (spaceP || Scan.succeed "") >> op^
   3.278 -        val (prewhs,rest1) = take_prefix (not o OuterLex.is_proper) (toks@sync)
   3.279 -        (* NB: this collapses  doclitcomment,(doclitcomment|whitespace)* to a single doclitcomment *)
   3.280 -        val (_,rest2) = (Scan.bulk (P.$$$ "--" |-- text_with_whs) >> implode || Scan.succeed "") rest1
   3.281 -        val (postwhs,rest3) = take_prefix (not o OuterLex.is_proper) rest2
   3.282 -    in
   3.283 -        ((markup_comment_whs prewhs) @
   3.284 -         (if (length rest2 = length rest1)  then []
   3.285 -          else 
   3.286 -	      (* These comments are "literate", but *not* counted for undo. So classify as ordinary comment. *)
   3.287 -	      [D.Comment 
   3.288 -		   {text= implode
   3.289 -                          (map OuterLex.unparse (Library.take (length rest1 - length rest2, rest1)))}]
   3.290 -              @
   3.291 -              (markup_comment_whs postwhs)),
   3.292 -              Library.take (length rest3 - 1,rest3))
   3.293 -    end
   3.294 -
   3.295 -fun xmls_of_impropers toks =
   3.296 -    let
   3.297 -        val (xmls,rest) = xmls_pre_cmd toks
   3.298 -	val unparsed =  
   3.299 -	    case rest of [] => []
   3.300 -		       | _ => [D.Unparseable 
   3.301 -			      {text= implode (map OuterLex.unparse rest)}]
   3.302 -    in
   3.303 -        xmls @ unparsed
   3.304 -    end
   3.305 -
   3.306 -end
   3.307 -
   3.308 -
   3.309 -local
   3.310 -    (* we have to weave together the whitespace/comments with proper tokens
   3.311 -       to reconstruct the input. *)
   3.312 -    (* TODO: see if duplicating isar_output/parse_thy can help here *)
   3.313 -
   3.314 -    fun match_tokens ([],us,vs) = (rev vs,us)  (* used, unused *)
   3.315 -      | match_tokens (t::ts, w::ws, vs) =
   3.316 -        if (t: OuterLex.token) = w  (* FIXME !? *)
   3.317 -          then match_tokens (ts, ws, w::vs)
   3.318 -          else match_tokens (t::ts, ws, w::vs)
   3.319 -      | match_tokens _ = error ("match_tokens: mismatched input parse")
   3.320 -in
   3.321 -    fun pgip_parser str =
   3.322 -    let
   3.323 -       (* parsing:   See outer_syntax.ML/toplevel_source *)
   3.324 -       fun parse_loop ([],[],xmls) = xmls
   3.325 -         | parse_loop ([],itoks,xmls) = xmls @ (xmls_of_impropers itoks)
   3.326 -         | parse_loop ((nm,toks,_)::trs,itoks,xmls) =
   3.327 -           let
   3.328 -               (* first proper token after whitespace/litcomment/whitespace is command *)
   3.329 -               val (xmls_pre_cmd,cmditoks') = xmls_pre_cmd itoks
   3.330 -               val (cmdtok,itoks') = 
   3.331 -		   case cmditoks' of x::xs => (x,xs)
   3.332 -                                   | _ => error("proof_general/parse_loop impossible")
   3.333 -               val (utoks,itoks'') = match_tokens (toks,itoks',[])
   3.334 -               (* FIXME: should take trailing [w/s+] semicolon too in utoks *)
   3.335 -
   3.336 -               val str = implode (map OuterLex.unparse (cmdtok::utoks))
   3.337 -
   3.338 -               val xmls_tr  = xmls_of_transition (nm,str,toks)
   3.339 -           in
   3.340 -               parse_loop(trs,itoks'',xmls @ xmls_pre_cmd @ xmls_tr)
   3.341 -           end
   3.342 -    in
   3.343 -        (let val toks = OuterSyntax.scan str
   3.344 -         in
   3.345 -             parse_loop (OuterSyntax.read toks, toks, [])
   3.346 -         end)
   3.347 -           handle _ => [D.Unparseable {text=str}]
   3.348 -    end
   3.349 -end
   3.350 -
   3.351 -end
     4.1 --- a/src/Pure/ProofGeneral/pgip_tests.ML	Sun Nov 04 16:43:31 2007 +0100
     4.2 +++ b/src/Pure/ProofGeneral/pgip_tests.ML	Sun Nov 04 17:12:14 2007 +0100
     4.3 @@ -108,14 +108,14 @@
     4.4  end
     4.5  
     4.6  
     4.7 -(** parsing.ML **)
     4.8 +(** pgip_parser.ML **)
     4.9  local
    4.10  open PgipMarkup
    4.11 -open OldPgipParser
    4.12 +open PgipParser
    4.13  open PgipIsabelle
    4.14  
    4.15  fun asseqp a b =
    4.16 -    if pgip_parser a = b then ()
    4.17 +    if pgip_parser Position.none a = b then ()
    4.18      else error("PGIP test: expected two parses to be equal, for input:\n" ^ a)
    4.19  
    4.20  in
     5.1 --- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Nov 04 16:43:31 2007 +0100
     5.2 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Sun Nov 04 17:12:14 2007 +0100
     5.3 @@ -1140,7 +1140,6 @@
     5.4    | init_pgip true =
     5.5        (! initialized orelse
     5.6          (Output.no_warnings init_outer_syntax ();
     5.7 -          OldPgipParser.init ();
     5.8            setup_preferences_tweak ();
     5.9            setup_proofgeneral_output ();
    5.10            setup_messages ();