src/Pure/Isar/outer_syntax.ML
changeset 7333 6cb15c6f1d9f
parent 7243 886ecd6a27ac
child 7367 a79d4683fadf
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Aug 24 11:50:34 1999 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Aug 24 11:50:58 1999 +0200
     1.3 @@ -51,7 +51,7 @@
     1.4    val theory_header: token list -> (string * string list * (string * bool) list) * token list
     1.5    val deps_thy: string -> Path.T -> string list * Path.T list
     1.6    val load_thy: string -> bool -> bool -> Path.T -> unit
     1.7 -  val isar: bool -> Toplevel.isar
     1.8 +  val isar: bool -> bool -> Toplevel.isar
     1.9  end;
    1.10  
    1.11  structure OuterSyntax: OUTER_SYNTAX =
    1.12 @@ -334,10 +334,10 @@
    1.13  
    1.14  (* interactive source of state transformers *)
    1.15  
    1.16 -fun isar term =
    1.17 +fun isar term no_pos =
    1.18    Source.tty
    1.19    |> Symbol.source true
    1.20 -  |> OuterLex.source true get_lexicons (Position.line_name 1 "stdin")
    1.21 +  |> OuterLex.source true get_lexicons (if no_pos then Position.none else Position.line_name 1 "stdin")
    1.22    |> source term true get_parser;
    1.23  
    1.24  
    1.25 @@ -346,18 +346,20 @@
    1.26  
    1.27  (* main loop *)
    1.28  
    1.29 -fun gen_loop term = (Context.reset_context (); Toplevel.loop (isar term));
    1.30 +fun gen_loop term no_pos =
    1.31 + (Context.reset_context ();
    1.32 +  Toplevel.loop (isar term no_pos));
    1.33  
    1.34 -fun gen_main term =
    1.35 +fun gen_main term no_pos =
    1.36   (Toplevel.set_state Toplevel.toplevel;
    1.37    ml_prompts "ML> " "ML# ";
    1.38    writeln (Session.welcome ());
    1.39 -  gen_loop term);
    1.40 +  gen_loop term no_pos);
    1.41  
    1.42 -fun main () = gen_main false;
    1.43 -fun loop () = gen_loop false;
    1.44 -fun sync_main () = gen_main true;
    1.45 -fun sync_loop () = gen_loop true;
    1.46 +fun main () = gen_main false false;
    1.47 +fun loop () = gen_loop false false;
    1.48 +fun sync_main () = gen_main true true;
    1.49 +fun sync_loop () = gen_loop true true;
    1.50  
    1.51  
    1.52  (* help *)