added read (provides transition names and sources);
authorwenzelm
Sat Jun 12 22:45:59 2004 +0200 (2004-06-12)
changeset 149250f86a8a694f8
parent 14924 2be4cbe27a27
child 14926 d2baf4b79424
added read (provides transition names and sources);
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Sat Jun 12 22:45:46 2004 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sat Jun 12 22:45:59 2004 +0200
     1.3 @@ -63,6 +63,7 @@
     1.4    val load_thy: string -> bool -> bool -> Path.T -> unit
     1.5    val isar: bool -> bool -> unit Toplevel.isar
     1.6    val isar_readstring: Position.T -> string -> (string list) Toplevel.isar
     1.7 +  val read: string -> (string * OuterLex.token list * Toplevel.transition) list
     1.8  end;
     1.9  
    1.10  structure OuterSyntax: OUTER_SYNTAX =
    1.11 @@ -123,20 +124,24 @@
    1.12  
    1.13  local
    1.14  
    1.15 -fun command_body cmd (name, _) =
    1.16 +fun terminate false = Scan.succeed ()
    1.17 +  | terminate true = P.group "end of input" (Scan.option P.sync -- P.semicolon >> K ());
    1.18 +
    1.19 +fun trace false parse = parse
    1.20 +  | trace true parse = Scan.trace parse >> (fn (f, toks) => f o Toplevel.source toks);
    1.21 +
    1.22 +fun body cmd trc (name, _) =
    1.23    (case cmd name of
    1.24 -    Some (int_only, parse) => P.!!! (Scan.prompt (name ^ "# ") (parse >> pair int_only))
    1.25 +    Some (int_only, parse) =>
    1.26 +      P.!!! (Scan.prompt (name ^ "# ") (trace trc parse >> pair int_only))
    1.27    | None => sys_error ("no parser for outer syntax command " ^ quote name));
    1.28  
    1.29 -fun terminator false = Scan.succeed ()
    1.30 -  | terminator true = P.group "end of input" (Scan.option P.sync -- P.semicolon >> K ());
    1.31 -
    1.32  in
    1.33  
    1.34 -fun command term cmd =
    1.35 +fun command do_terminate do_trace cmd =
    1.36    P.semicolon >> K None ||
    1.37    P.sync >> K None ||
    1.38 -  (P.position P.command :-- command_body cmd) --| terminator term
    1.39 +  (P.position P.command :-- body cmd do_trace) --| terminate do_terminate
    1.40      >> (fn ((name, pos), (int_only, f)) =>
    1.41        Some (Toplevel.empty |> Toplevel.name name |> Toplevel.position pos |>
    1.42          Toplevel.interactive int_only |> f));
    1.43 @@ -232,7 +237,7 @@
    1.44  
    1.45  (* basic sources *)
    1.46  
    1.47 -fun toplevel_source term do_recover cmd src =
    1.48 +fun toplevel_source term trc do_recover cmd src =
    1.49    let
    1.50      val no_terminator =
    1.51        Scan.unless P.semicolon (Scan.one (T.not_sync andf T.not_eof));
    1.52 @@ -244,7 +249,7 @@
    1.53        (Scan.bulk (P.$$$ "--" -- P.!!! P.text >> K None || P.not_eof >> Some))
    1.54        (if do_recover then Some recover else None)
    1.55      |> Source.mapfilter I
    1.56 -    |> Source.source T.stopper (Scan.bulk (fn xs => P.!!! (command term (cmd ())) xs))
    1.57 +    |> Source.source T.stopper (Scan.bulk (fn xs => P.!!! (command term trc (cmd ())) xs))
    1.58        (if do_recover then Some recover else None)
    1.59      |> Source.mapfilter I
    1.60    end;
    1.61 @@ -257,16 +262,27 @@
    1.62    |> Symbol.source true
    1.63    |> T.source true get_lexicons
    1.64      (if no_pos then Position.none else Position.line_name 1 "stdin")
    1.65 -  |> toplevel_source term true get_parser;
    1.66 +  |> toplevel_source term false true get_parser;
    1.67  
    1.68  
    1.69 -(* string source of transformers (for Proof General) *)
    1.70 +(* string source of transformers with trace (for Proof General) *)
    1.71  
    1.72  fun isar_readstring pos str =
    1.73    Source.of_string str
    1.74    |> Symbol.source false
    1.75    |> T.source false get_lexicons pos
    1.76 -  |> toplevel_source false true get_parser;
    1.77 +  |> toplevel_source false true true get_parser;
    1.78 +
    1.79 +
    1.80 +(* read text -- with trace of source *)
    1.81 +
    1.82 +fun read str =
    1.83 +  Source.of_string str
    1.84 +  |> Symbol.source false
    1.85 +  |> T.source false get_lexicons Position.none
    1.86 +  |> toplevel_source false true true get_parser
    1.87 +  |> Source.exhaust
    1.88 +  |> map (fn tr => (Toplevel.name_of tr, the (Toplevel.source_of tr), tr));
    1.89  
    1.90  
    1.91  
    1.92 @@ -311,7 +327,7 @@
    1.93  
    1.94  fun parse_thy src =
    1.95    src
    1.96 -  |> toplevel_source false false (K (get_parser ()))
    1.97 +  |> toplevel_source false false false (K (get_parser ()))
    1.98    |> Source.exhaust;
    1.99  
   1.100  fun run_thy name path =