# HG changeset patch # User wenzelm # Date 930738226 -7200 # Node ID 8dc6a1e6fa13688b766221a2088d7412c3b6279a # Parent 2b3db2b6c1293d1df5454855e5f7d8f82479c643 added sync; diff -r 2b3db2b6c129 -r 8dc6a1e6fa13 src/Pure/Isar/outer_parse.ML --- a/src/Pure/Isar/outer_parse.ML Wed Jun 30 12:23:34 1999 +0200 +++ b/src/Pure/Isar/outer_parse.ML Wed Jun 30 12:23:46 1999 +0200 @@ -23,6 +23,7 @@ val number: token list -> string * token list val string: token list -> string * token list val verbatim: token list -> string * token list + val sync: token list -> string * token list val eof: token list -> string * token list val not_eof: token list -> token * token list val nat: token list -> int * token list @@ -122,6 +123,7 @@ val number = kind OuterLex.Nat; val string = kind OuterLex.String; val verbatim = kind OuterLex.Verbatim; +val sync = kind OuterLex.Sync; val eof = kind OuterLex.EOF; fun $$$ x = diff -r 2b3db2b6c129 -r 8dc6a1e6fa13 src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Wed Jun 30 12:23:34 1999 +0200 +++ b/src/Pure/Isar/outer_syntax.ML Wed Jun 30 12:23:46 1999 +0200 @@ -13,6 +13,8 @@ sig val main: unit -> unit val loop: unit -> unit + val sync_main: unit -> unit + val sync_loop: unit -> unit val help: unit -> unit end; @@ -50,12 +52,14 @@ 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 + val isar: bool -> Toplevel.isar end; structure OuterSyntax: OUTER_SYNTAX = struct +structure P = OuterParse; + (** outer syntax **) @@ -96,21 +100,28 @@ (* parse command *) -local open OuterParse in +local fun command_name cmd = - group "command" - (position (Scan.one (OuterLex.keyword_pred (is_some o cmd)) >> OuterLex.val_of)); + P.group "command" + (P.position (Scan.one (OuterLex.keyword_pred (is_some o cmd)) >> OuterLex.val_of)); fun command_body cmd (name, _) = let val (int_only, parse) = the (cmd name) - in !!! (Scan.prompt (name ^ "# ") (parse >> pair int_only)) end; + in P.!!! (Scan.prompt (name ^ "# ") (parse >> pair int_only)) end; + +fun terminator false = Scan.succeed () + | terminator true = P.group "terminator" (Scan.option P.sync -- P.$$$ ";" >> K ()); + +in -fun command cmd = - $$$ ";" >> K None || - command_name cmd :-- command_body cmd >> (fn ((name, pos), (int_only, f)) => - Some (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |> - Toplevel.interactive int_only |> f)); +fun command term cmd = + P.$$$ ";" >> K None || + P.sync >> K None || + (command_name cmd :-- command_body cmd) --| terminator term + >> (fn ((name, pos), (int_only, f)) => + Some (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |> + Toplevel.interactive int_only |> f)); end; @@ -177,18 +188,24 @@ (* source *) -fun no_command cmd = - Scan.one ((not o OuterLex.keyword_pred ((is_some o cmd) orf equal ";")) andf OuterLex.not_eof); +local -fun recover cmd = - Scan.prompt "recover# " (Scan.one OuterLex.not_eof -- Scan.repeat (no_command cmd)); +val no_terminator = + Scan.unless (P.$$$ ";") (Scan.one (OuterLex.not_sync andf OuterLex.not_eof)); + +val recover = Scan.prompt "recover# " (Scan.repeat no_terminator); + +in -fun source do_recover cmd src = +fun source term do_recover cmd src = src - |> Source.source OuterLex.stopper (Scan.bulk (fn xs => OuterParse.!!! (command (cmd ())) xs)) - (if do_recover then Some (fn xs => recover (cmd ()) xs) else None) + |> Source.source OuterLex.stopper + (Scan.bulk (fn xs => OuterParse.!!! (command term (cmd ())) xs)) + (if do_recover then Some recover else None) |> Source.mapfilter I; +end; + (* detect header *) @@ -216,21 +233,23 @@ val header_lexicon = Scan.make_lexicon (map Symbol.explode ["(", ")", "+", ":", "=", "files", theoryN]); -local open OuterParse in +local -val file_name = ($$$ "(" |-- !!! (name --| $$$ ")")) >> rpair false || name >> rpair true; +val file_name = (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) >> rpair false || P.name >> rpair true; val theory_head = - (name -- ($$$ "=" |-- enum1 "+" name) -- - Scan.optional ($$$ "files" |-- !!! (Scan.repeat1 file_name)) []) + (P.name -- (P.$$$ "=" |-- P.enum1 "+" P.name) -- + Scan.optional (P.$$$ "files" |-- P.!!! (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; +in + +val theory_header = theory_head --| (Scan.ahead P.eof || P.$$$ ":"); +val only_header = theory_keyword |-- theory_head --| Scan.ahead P.eof; +val new_header = theory_keyword |-- P.!!! theory_header; val old_header = - name -- ($$$ "=" |-- name -- Scan.repeat ($$$ "+" |-- name)) + P.name -- (P.$$$ "=" |-- P.name -- Scan.repeat (P.$$$ "+" |-- P.name)) >> (fn (A, (B, Bs)) => (A, B :: Bs, []: (string * bool) list)); end; @@ -279,7 +298,7 @@ (case only_head of None => lex_src - |> source false (K (get_parser ())) + |> source false false (K (get_parser ())) |> Source.exhaust | Some spec => [Toplevel.empty |> Toplevel.name theoryN |> IsarThy.theory spec, @@ -307,11 +326,11 @@ (* interactive source of state transformers *) -val isar = +fun isar term = Source.tty |> Symbol.source true |> OuterLex.source true get_lexicon (Position.line_name 1 "stdin") - |> source true get_parser; + |> source term true get_parser; @@ -319,13 +338,18 @@ (* main loop *) -fun loop () = (Context.reset_context (); Toplevel.loop isar); +fun gen_loop term = (Context.reset_context (); Toplevel.loop (isar term)); -fun main () = +fun gen_main term = (Toplevel.set_state Toplevel.toplevel; ml_prompts "ML> " "ML# "; writeln (Session.welcome ()); - loop ()); + gen_loop term); + +fun main () = gen_main false; +fun loop () = gen_loop false; +fun sync_main () = gen_main true; +fun sync_loop () = gen_loop true; (* help *)