77 val closure_src: src -> src |
77 val closure_src: src -> src |
78 val pretty_value: Proof.context -> T -> Pretty.T |
78 val pretty_value: Proof.context -> T -> Pretty.T |
79 val pretty_src: Proof.context -> src -> Pretty.T |
79 val pretty_src: Proof.context -> src -> Pretty.T |
80 val ident_or_symbolic: string -> bool |
80 val ident_or_symbolic: string -> bool |
81 val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source |
81 val source_proper: (T, 'a) Source.source -> (T, (T, 'a) Source.source) Source.source |
82 val source': {do_recover: bool option} -> (unit -> Scan.lexicon * Scan.lexicon) -> |
82 val source': {do_recover: bool} -> (unit -> Scan.lexicon * Scan.lexicon) -> |
83 (Symbol_Pos.T, 'a) Source.source -> (T, (Symbol_Pos.T, 'a) Source.source) Source.source |
83 (Symbol_Pos.T, 'a) Source.source -> (T, (Symbol_Pos.T, 'a) Source.source) Source.source |
84 val source: {do_recover: bool option} -> (unit -> Scan.lexicon * Scan.lexicon) -> |
84 val source: {do_recover: bool} -> (unit -> Scan.lexicon * Scan.lexicon) -> |
85 Position.T -> (Symbol.symbol, 'a) Source.source -> (T, |
85 Position.T -> (Symbol.symbol, 'a) Source.source -> (T, |
86 (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source |
86 (Symbol_Pos.T, Position.T * (Symbol.symbol, 'a) Source.source) Source.source) Source.source |
87 type 'a parser = T list -> 'a * T list |
87 type 'a parser = T list -> 'a * T list |
88 type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list) |
88 type 'a context_parser = Context.generic * T list -> 'a * (Context.generic * T list) |
89 val read: Scan.lexicon -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a list |
89 val read: Scan.lexicon -> 'a parser -> Symbol_Pos.T list * Position.T -> 'a list |
560 |
560 |
561 in |
561 in |
562 |
562 |
563 fun source' {do_recover} get_lex = |
563 fun source' {do_recover} get_lex = |
564 Source.source Symbol_Pos.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs)) |
564 Source.source Symbol_Pos.stopper (Scan.bulk (fn xs => scan (get_lex ()) xs)) |
565 (Option.map (rpair recover) do_recover); |
565 (if do_recover then SOME recover else NONE); |
566 |
566 |
567 fun source do_recover get_lex pos src = |
567 fun source do_recover get_lex pos src = |
568 Symbol_Pos.source pos src |
568 Symbol_Pos.source pos src |
569 |> source' do_recover get_lex; |
569 |> source' do_recover get_lex; |
570 |
570 |
580 |
580 |
581 (* read source *) |
581 (* read source *) |
582 |
582 |
583 fun read lex scan (syms, pos) = |
583 fun read lex scan (syms, pos) = |
584 Source.of_list syms |
584 Source.of_list syms |
585 |> source' {do_recover = NONE} (K (lex, Scan.empty_lexicon)) |
585 |> source' {do_recover = false} (K (lex, Scan.empty_lexicon)) |
586 |> source_proper |
586 |> source_proper |
587 |> Source.source stopper (Scan.error (Scan.bulk scan)) NONE |
587 |> Source.source stopper (Scan.error (Scan.bulk scan)) NONE |
588 |> Source.exhaust; |
588 |> Source.exhaust; |
589 |
589 |
590 fun read_antiq lex scan (syms, pos) = |
590 fun read_antiq lex scan (syms, pos) = |