export token_source;
authorwenzelm
Sun Oct 03 15:52:53 1999 +0200 (1999-10-03)
changeset 7683e74f43f1d8a3
parent 7682 46de8064c93c
child 7684 2e691e52281d
export token_source;
improved Present.theory_source;
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Sun Oct 03 15:51:38 1999 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sun Oct 03 15:52:53 1999 +0200
     1.3 @@ -50,6 +50,8 @@
     1.4    val print_help: Toplevel.transition -> Toplevel.transition
     1.5    val add_keywords: string list -> unit
     1.6    val add_parsers: parser list -> unit
     1.7 +  val token_source: (string, 'a) Source.source * Position.T -> (OuterLex.token,
     1.8 +    Position.T * (Symbol.symbol, (string, 'a) Source.source) Source.source) Source.source
     1.9    val theory_header: token list -> (string * string list * (string * bool) list) * token list
    1.10    val deps_thy: string -> Path.T -> string list * Path.T list
    1.11    val load_thy: string -> bool -> bool -> Path.T -> unit
    1.12 @@ -212,7 +214,7 @@
    1.13  val theory_keyword = OuterParse.$$$ theoryN;
    1.14  
    1.15  
    1.16 -(* source *)
    1.17 +(* sources *)
    1.18  
    1.19  local
    1.20  
    1.21 @@ -232,6 +234,15 @@
    1.22  
    1.23  end;
    1.24  
    1.25 +fun token_source (src, pos) =
    1.26 +  src
    1.27 +  |> Symbol.source false
    1.28 +  |> OuterLex.source false (K (get_lexicons ())) pos;
    1.29 +
    1.30 +fun filter_proper src =
    1.31 +  src
    1.32 +  |> Source.filter OuterLex.is_proper;
    1.33 +
    1.34  
    1.35  (* detect header *)
    1.36  
    1.37 @@ -239,6 +250,7 @@
    1.38    src
    1.39    |> Symbol.source false
    1.40    |> OuterLex.source false (fn () => (get_lex (), Scan.empty_lexicon)) pos
    1.41 +  |> filter_proper
    1.42    |> Source.source OuterLex.stopper (Scan.single scan) None
    1.43    |> (fst o the o Source.get_single);
    1.44  
    1.45 @@ -304,12 +316,9 @@
    1.46      else Toplevel.excursion_error [Toplevel.empty |> Toplevel.name tr_name |> tr]
    1.47    end;
    1.48  
    1.49 -fun parse_thy (src, pos) =
    1.50 +fun parse_thy src_pos =
    1.51    let
    1.52 -    val lex_src =
    1.53 -      src
    1.54 -      |> Symbol.source false
    1.55 -      |> OuterLex.source false (K (get_lexicons ())) pos;
    1.56 +    val lex_src = filter_proper (token_source src_pos);
    1.57      val only_head =
    1.58        lex_src
    1.59        |> Source.source OuterLex.stopper (Scan.single (Scan.option only_header)) None
    1.60 @@ -326,9 +335,12 @@
    1.61    end;
    1.62  
    1.63  fun run_thy name path =
    1.64 -  let val (src, pos) = File.source path in
    1.65 -    Present.theory_source name src;
    1.66 -    if is_old_theory (src, pos) then ThySyn.load_thy name (Source.exhaust src)
    1.67 +  let
    1.68 +    val (src, pos) = File.source path;
    1.69 +    val is_old = is_old_theory (src, pos);
    1.70 +  in
    1.71 +    Present.theory_source is_old name (src, pos);
    1.72 +    if is_old then ThySyn.load_thy name (Source.exhaust src)
    1.73      else Toplevel.excursion_error (parse_thy (src, pos))
    1.74    end;
    1.75  
    1.76 @@ -350,6 +362,7 @@
    1.77    |> Symbol.source true
    1.78    |> OuterLex.source true get_lexicons
    1.79      (if no_pos then Position.none else Position.line_name 1 "stdin")
    1.80 +  |> filter_proper
    1.81    |> source term true get_parser;
    1.82  
    1.83