added ProofGeneral/pgip_parser.ML;
authorwenzelm
Thu Jul 12 00:15:26 2007 +0200 (2007-07-12)
changeset 23793b04afc51914c
parent 23792 1bca2cea80e0
child 23794 ab2edd87b912
added ProofGeneral/pgip_parser.ML;
src/Pure/IsaMakefile
src/Pure/ProofGeneral/ROOT.ML
     1.1 --- a/src/Pure/IsaMakefile	Wed Jul 11 19:22:05 2007 +0200
     1.2 +++ b/src/Pure/IsaMakefile	Thu Jul 12 00:15:26 2007 +0200
     1.3 @@ -48,23 +48,23 @@
     1.4    Proof/proofchecker.ML Proof/reconstruct.ML Pure.thy ROOT.ML			\
     1.5    ProofGeneral/parsing.ML ProofGeneral/pgip_input.ML 				\
     1.6    ProofGeneral/pgip_isabelle.ML ProofGeneral/pgip_markup.ML			\
     1.7 -  ProofGeneral/pgip.ML ProofGeneral/pgip_output.ML ProofGeneral/pgip_tests.ML	\
     1.8 -  ProofGeneral/pgip_types.ML ProofGeneral/preferences.ML			\
     1.9 -  ProofGeneral/proof_general_pgip.ML ProofGeneral/proof_general_emacs.ML	\
    1.10 -  ProofGeneral/ROOT.ML Syntax/ast.ML Syntax/lexicon.ML Syntax/mixfix.ML		\
    1.11 -  Syntax/parser.ML Syntax/printer.ML Syntax/syn_ext.ML Syntax/syn_trans.ML	\
    1.12 -  Syntax/syntax.ML Syntax/type_ext.ML Thy/html.ML Thy/latex.ML 			\
    1.13 -  Thy/ml_context.ML Thy/present.ML Thy/term_style.ML Thy/thm_database.ML	\
    1.14 -  Thy/thm_deps.ML Thy/thy_edit.ML Thy/thy_header.ML Thy/thy_info.ML 		\
    1.15 -  Thy/thy_load.ML Thy/thy_output.ML Tools/ROOT.ML Tools/class_package.ML	\
    1.16 -  Tools/codegen_consts.ML Tools/codegen_data.ML Tools/codegen_func.ML 		\
    1.17 -  Tools/codegen_funcgr.ML Tools/codegen_names.ML Tools/codegen_package.ML 	\
    1.18 -  Tools/codegen_serializer.ML Tools/codegen_thingol.ML Tools/invoke.ML		\
    1.19 -  Tools/nbe.ML Tools/nbe_codegen.ML Tools/nbe_eval.ML Tools/xml.ML 		\
    1.20 -  Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML compress.ML		\
    1.21 -  conjunction.ML consts.ML context.ML context_position.ML conv.ML defs.ML	\
    1.22 -  display.ML drule.ML envir.ML fact_index.ML goal.ML install_pp.ML library.ML 	\
    1.23 -  logic.ML meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML 		\
    1.24 +  ProofGeneral/pgip.ML ProofGeneral/pgip_output.ML ProofGeneral/pgip_parser.ML	\
    1.25 +  ProofGeneral/pgip_tests.ML ProofGeneral/pgip_types.ML				\
    1.26 +  ProofGeneral/preferences.ML ProofGeneral/proof_general_pgip.ML		\
    1.27 +  ProofGeneral/proof_general_emacs.ML ProofGeneral/ROOT.ML Syntax/ast.ML	\
    1.28 +  Syntax/lexicon.ML Syntax/mixfix.ML Syntax/parser.ML Syntax/printer.ML		\
    1.29 +  Syntax/syn_ext.ML Syntax/syn_trans.ML Syntax/syntax.ML Syntax/type_ext.ML	\
    1.30 +  Thy/html.ML Thy/latex.ML Thy/ml_context.ML Thy/present.ML Thy/term_style.ML	\
    1.31 +  Thy/thm_database.ML Thy/thm_deps.ML Thy/thy_edit.ML Thy/thy_header.ML		\
    1.32 +  Thy/thy_info.ML Thy/thy_load.ML Thy/thy_output.ML Tools/ROOT.ML		\
    1.33 +  Tools/class_package.ML Tools/codegen_consts.ML Tools/codegen_data.ML		\
    1.34 +  Tools/codegen_func.ML Tools/codegen_funcgr.ML Tools/codegen_names.ML		\
    1.35 +  Tools/codegen_package.ML Tools/codegen_serializer.ML Tools/codegen_thingol.ML	\
    1.36 +  Tools/invoke.ML Tools/nbe.ML Tools/nbe_codegen.ML Tools/nbe_eval.ML		\
    1.37 +  Tools/xml.ML Tools/xml_syntax.ML assumption.ML axclass.ML codegen.ML		\
    1.38 +  compress.ML conjunction.ML consts.ML context.ML context_position.ML conv.ML	\
    1.39 +  defs.ML display.ML drule.ML envir.ML fact_index.ML goal.ML install_pp.ML 	\
    1.40 +  library.ML logic.ML meta_simplifier.ML more_thm.ML morphism.ML name.ML net.ML	\
    1.41    old_goals.ML pattern.ML proofterm.ML pure_thy.ML search.ML sign.ML 		\
    1.42    simplifier.ML sorts.ML subgoal.ML tactic.ML tctical.ML term.ML term_subst.ML	\
    1.43    theory.ML thm.ML type.ML type_infer.ML unify.ML variable.ML
     2.1 --- a/src/Pure/ProofGeneral/ROOT.ML	Wed Jul 11 19:22:05 2007 +0200
     2.2 +++ b/src/Pure/ProofGeneral/ROOT.ML	Thu Jul 12 00:15:26 2007 +0200
     2.3 @@ -15,7 +15,9 @@
     2.4  use "pgip_isabelle.ML";
     2.5  use "pgml_isabelle.ML";
     2.6  use "preferences.ML";
     2.7 -use "parsing.ML";
     2.8 +use "pgip_parser.ML";
     2.9 +
    2.10 +use "parsing.ML";   (* old version *)
    2.11  
    2.12  use "pgip_tests.ML";
    2.13