toplevel_source: interactive flag indicates intermittent error_msg;
authorwenzelm
Mon Jul 09 23:12:46 2007 +0200 (2007-07-09)
changeset 2367957dceb84d1a0
parent 23678 f5d315390edc
child 23680 09ccdb1b93ba
toplevel_source: interactive flag indicates intermittent error_msg;
nested source: error msg passed to recover;
tuned source positions;
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Mon Jul 09 23:12:45 2007 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Mon Jul 09 23:12:46 2007 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4    val check_text: string * Position.T -> Toplevel.node option -> unit
     1.5    val deps_thy: string -> bool -> Path.T -> string list * Path.T list
     1.6    val load_thy: string -> bool -> bool -> Path.T -> unit
     1.7 -  val isar: bool -> bool -> unit Toplevel.isar
     1.8 +  val isar: bool -> unit Toplevel.isar
     1.9    val scan: string -> OuterLex.token list
    1.10    val read: OuterLex.token list -> (string * OuterLex.token list * Toplevel.transition) list
    1.11  end;
    1.12 @@ -192,28 +192,29 @@
    1.13    let
    1.14      val no_terminator =
    1.15        Scan.unless P.semicolon (Scan.one (T.not_sync andf T.not_eof));
    1.16 -    fun recover x = (Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]) x;
    1.17 +    fun recover interactive msg x =
    1.18 +      (if interactive then Output.error_msg msg else ();
    1.19 +        (Scan.prompt "recover# " (Scan.repeat no_terminator) >> K [NONE]) x);
    1.20    in
    1.21      src
    1.22      |> T.source_proper
    1.23      |> Source.source T.stopper
    1.24        (Scan.bulk (P.$$$ "--" -- P.!!! P.text >> K NONE || P.not_eof >> SOME))
    1.25 -      (if do_recover then SOME recover else NONE)
    1.26 +      (Option.map recover do_recover)
    1.27      |> Source.map_filter I
    1.28      |> Source.source T.stopper (Scan.bulk (fn xs => P.!!! (command term do_trace (cmd ())) xs))
    1.29 -      (if do_recover then SOME recover else NONE)
    1.30 +      (Option.map recover do_recover)
    1.31      |> Source.map_filter I
    1.32    end;
    1.33  
    1.34  
    1.35  (* interactive source of toplevel transformers *)
    1.36  
    1.37 -fun isar term no_pos =
    1.38 +fun isar term =
    1.39    Source.tty
    1.40    |> Symbol.source true
    1.41 -  |> T.source true get_lexicons
    1.42 -    (if no_pos then Position.none else Position.line_name 1 "stdin")
    1.43 -  |> toplevel_source term false true get_parser;
    1.44 +  |> T.source (SOME true) get_lexicons Position.none
    1.45 +  |> toplevel_source term false (SOME true) get_parser;
    1.46  
    1.47  
    1.48  (* scan text *)
    1.49 @@ -221,7 +222,7 @@
    1.50  fun scan str =
    1.51    Source.of_string str
    1.52    |> Symbol.source false
    1.53 -  |> T.source true get_lexicons Position.none
    1.54 +  |> T.source (SOME false) get_lexicons Position.none
    1.55    |> Source.exhaust;
    1.56  
    1.57  
    1.58 @@ -229,7 +230,7 @@
    1.59  
    1.60  fun read toks =
    1.61    Source.of_list toks
    1.62 -  |> toplevel_source false true true get_parser
    1.63 +  |> toplevel_source false true (SOME false) get_parser
    1.64    |> Source.exhaust
    1.65    |> map (fn tr => (Toplevel.name_of tr, the (Toplevel.source_of tr), tr));
    1.66  
    1.67 @@ -247,7 +248,7 @@
    1.68  fun deps_thy name ml path =
    1.69    let
    1.70      val src = Source.of_string (File.read path);
    1.71 -    val pos = Path.position path;
    1.72 +    val pos = Position.path path;
    1.73      val (name', parents, files) = ThyHeader.read (src, pos);
    1.74      val ml_path = ThyLoad.ml_path name;
    1.75      val ml_file = if ml andalso is_some (ThyLoad.check_file NONE ml_path) then [ml_path] else [];
    1.76 @@ -281,10 +282,10 @@
    1.77      val _ = Present.verbatim_source name (fn () => Source.exhaust (Symbol.source false text));
    1.78      val toks = text
    1.79        |> Symbol.source false
    1.80 -      |> T.source false (K (get_lexicons ())) (Path.position path)
    1.81 +      |> T.source NONE (K (get_lexicons ())) (Position.path path)
    1.82        |> Source.exhausted;
    1.83      val trs = toks
    1.84 -      |> toplevel_source false false false (K (get_parser ()))
    1.85 +      |> toplevel_source false false NONE (K (get_parser ()))
    1.86        |> Source.exhaust;
    1.87    in
    1.88      ThyOutput.present_thy (#1 (get_lexicons ())) command_tags is_markup trs toks
    1.89 @@ -312,14 +313,14 @@
    1.90  
    1.91  (* main loop *)
    1.92  
    1.93 -fun gen_loop term no_pos =
    1.94 +fun gen_loop term =
    1.95   (ML_Context.set_context NONE;
    1.96 -  Toplevel.loop (isar term no_pos));
    1.97 +  Toplevel.loop (isar term));
    1.98  
    1.99 -fun gen_main term no_pos =
   1.100 +fun gen_main term =
   1.101   (Toplevel.init_state ();
   1.102    writeln (Session.welcome ());
   1.103 -  gen_loop term no_pos);
   1.104 +  gen_loop term);
   1.105  
   1.106  structure Isar =
   1.107  struct
   1.108 @@ -334,10 +335,10 @@
   1.109      #2 (Proof.get_goal (Toplevel.proof_of (state ())))
   1.110        handle Toplevel.UNDEF => error "No goal present";
   1.111  
   1.112 -  fun main () = gen_main false false;
   1.113 -  fun loop () = gen_loop false false;
   1.114 -  fun sync_main () = gen_main true true;
   1.115 -  fun sync_loop () = gen_loop true true;
   1.116 +  fun main () = gen_main false;
   1.117 +  fun loop () = gen_loop false;
   1.118 +  fun sync_main () = gen_main true;
   1.119 +  fun sync_loop () = gen_loop true;
   1.120    val toplevel = Toplevel.program;
   1.121  end;
   1.122