# HG changeset patch # User wenzelm # Date 918245184 -3600 # Node ID e8bbe64861b88aa3c2d4586530b08c719f60aaa1 # Parent 0aa2e536bc2087e665e8f92533bfc37ee8c73da7 more robust handling of theory context; header-only theory files; diff -r 0aa2e536bc20 -r e8bbe64861b8 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Fri Feb 05 21:04:58 1999 +0100 +++ b/src/Pure/Isar/outer_syntax.ML Fri Feb 05 21:06:24 1999 +0100 @@ -3,6 +3,10 @@ Author: Markus Wenzel, TU Muenchen The global Isabelle/Isar outer syntax. + +TODO: + - cleanup; + - avoid string constants; *) signature BASIC_OUTER_SYNTAX = @@ -23,6 +27,7 @@ val commands: unit -> string list val add_keywords: string list -> unit val add_parsers: parser list -> unit + val theory_header: token list -> (string * string list * (string * bool) list) * token list val deps_thy: string -> bool -> Path.T -> string list * Path.T list val load_thy: string -> bool -> bool -> Path.T -> unit val isar: Toplevel.isar @@ -118,6 +123,12 @@ (** read theory **) +(* theory keyword *) + +val theoryN = "theory"; +val theory_keyword = OuterParse.$$$ theoryN; + + (* source *) fun no_command cmd = @@ -142,10 +153,10 @@ |> Source.source OuterLex.stopper (Scan.single scan) None |> (fst o the o Source.get_single); -val check_header_lexicon = Scan.make_lexicon [Symbol.explode "theory"]; +val check_header_lexicon = Scan.make_lexicon [Symbol.explode theoryN]; fun is_old_theory src = - is_none (scan_header (K check_header_lexicon) (Scan.option (OuterParse.$$$ "theory")) src); + is_none (scan_header (K check_header_lexicon) (Scan.option theory_keyword) src); fun warn_theory_style path is_old = let @@ -156,18 +167,25 @@ (* deps_thy --- inspect theory header *) -val new_header_lexicon = - Scan.make_lexicon (map Symbol.explode ["+", ":", "=", "files", "theory"]); +val header_lexicon = + Scan.make_lexicon (map Symbol.explode ["(", ")", "+", ":", "=", "files", theoryN]); local open OuterParse in -val new_header = - $$$ "theory" |-- !!! (name -- ($$$ "=" |-- enum1 "+" name) -- - Scan.optional ($$$ "files" |-- !!! (Scan.repeat1 name)) [] --| (Scan.ahead eof || $$$ ":")); +val file_name = ($$$ "(" |-- !!! (name --| $$$ ")")) >> rpair false || name >> rpair true; + +val theory_head = + (name -- ($$$ "=" |-- enum1 "+" name) -- + Scan.optional ($$$ "files" |-- !!! (Scan.repeat1 file_name)) []) + >> (fn ((A, Bs), files) => (A, Bs, files)); + +val theory_header = theory_head --| (Scan.ahead eof || $$$ ":"); +val only_header = theory_keyword |-- theory_head --| Scan.ahead eof; +val new_header = theory_keyword |-- !!! theory_header; val old_header = name -- ($$$ "=" |-- name -- Scan.repeat ($$$ "+" |-- name)) - >> (fn (A, (B, Bs)) => ((A, B :: Bs), []: string list)); + >> (fn (A, (B, Bs)) => (A, B :: Bs, []: (string * bool) list)); end; @@ -175,53 +193,69 @@ let val src = Source.of_file path; val is_old = warn_theory_style path (is_old_theory src); - val ((name', parents), files) = + val (name', parents, files) = (*Note: old style headers dynamically depend on the current lexicon :-( *) if is_old then scan_header ThySyn.get_lexicon (Scan.error old_header) src - else scan_header (K new_header_lexicon) (Scan.error new_header) src; + else scan_header (K header_lexicon) (Scan.error new_header) src; val ml_path = ThyLoad.ml_path name; val ml_file = if not ml orelse is_none (ThyLoad.check_file ml_path) then [] else [ml_path]; in if name <> name' then error ("Filename " ^ quote (Path.pack path) ^ " does not match theory name " ^ quote name) - else (parents, map Path.unpack files @ ml_file) + else (parents, map (Path.unpack o #1) files @ ml_file) end; (* load_thy --- read text (including header) *) -fun try_ml_file name ml = +fun try_ml_file name ml time = let val path = ThyLoad.ml_path name; - val tr = Toplevel.imperative (fn () => ThyInfo.load_file path); + val tr = Toplevel.imperative (fn () => ThyInfo.load_file time path); + val tr_name = if time then "time_use" else "use"; in if not ml orelse is_none (ThyLoad.check_file path) then () - else Toplevel.excursion [Toplevel.empty |> Toplevel.name "use" |> tr] + else Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr] end; fun parse_thy (src, pos) = - src - |> Symbol.source false - |> OuterLex.source false (K (get_lexicon ())) pos - |> source false (K (get_parser ())) - |> Source.exhaust; + let + val lex_src = + src + |> Symbol.source false + |> OuterLex.source false (K (get_lexicon ())) pos; + val only_head = + lex_src + |> Source.source OuterLex.stopper (Scan.single (Scan.option only_header)) None + |> (fst o the o Source.get_single); + in + (case only_head of + None => + lex_src + |> source false (K (get_parser ())) + |> Source.exhaust + | Some spec => + [Toplevel.empty |> Toplevel.name theoryN |> IsarThy.theory spec, + Toplevel.empty |> Toplevel.name "end" |> Toplevel.exit]) + end; -fun read_thy name ml path = - let - val (src, pos) = Source.of_file path; - val _ = - if is_old_theory (src, pos) then ThySyn.load_thy name (Source.exhaust src) - else (Toplevel.excursion (parse_thy (src, pos)) - handle exn => error (Toplevel.exn_message exn)); - in Context.context (ThyInfo.get_theory name); try_ml_file name ml end; +fun run_thy name path = + let val (src, pos) = Source.of_file path in + if is_old_theory (src, pos) then ThySyn.load_thy name (Source.exhaust src) + else (Toplevel.excursion (parse_thy (src, pos)) + handle exn => error (Toplevel.exn_message exn)) + end; fun load_thy name ml time path = - if not time then read_thy name ml path - else timeit (fn () => - (writeln ("\n**** Starting Theory " ^ quote name ^ " ****"); - setmp Goals.proof_timing true (read_thy name ml) path; - writeln ("**** Finished Theory " ^ quote name ^ " ****\n"))); + (if time then + timeit (fn () => + (writeln ("\n**** Starting theory " ^ quote name ^ " ****"); + setmp Goals.proof_timing true (run_thy name) path; + writeln ("**** Finished theory " ^ quote name ^ " ****\n"))) + else run_thy name path; + Context.context (ThyInfo.get_theory name); + try_ml_file name ml time); (* interactive source of state transformers *)