# HG changeset patch # User wenzelm # Date 1361723395 -3600 # Node ID fcc4b89a600db8f7cc4bcd27d7fe147e7fe67b81 # Parent c68c1b89a0f1f2a1109f4570bc0f9d7d6b12477d simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored; eliminated separate Outer_Syntax.read_element; diff -r c68c1b89a0f1 -r fcc4b89a600d src/Pure/Isar/outer_syntax.ML --- a/src/Pure/Isar/outer_syntax.ML Sun Feb 24 14:14:07 2013 +0100 +++ b/src/Pure/Isar/outer_syntax.ML Sun Feb 24 17:29:55 2013 +0100 @@ -35,9 +35,7 @@ type isar val isar: TextIO.instream -> bool -> isar val span_cmts: Token.T list -> Token.T list - val read_span: outer_syntax -> Token.T list -> Toplevel.transition * bool - val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.span Thy_Syntax.element -> - (Toplevel.transition * Toplevel.transition list) list + val read_span: outer_syntax -> Token.T list -> Toplevel.transition end; structure Outer_Syntax: OUTER_SYNTAX = @@ -319,30 +317,16 @@ val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens toks; val _ = Position.reports_text (token_reports @ maps command_reports toks); in - if is_malformed then (Toplevel.malformed pos "Malformed command syntax", true) + if is_malformed then Toplevel.malformed pos "Malformed command syntax" else (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of [tr] => if Keyword.is_control (Toplevel.name_of tr) then - (Toplevel.malformed pos "Illegal control command", true) - else (tr, true) - | [] => (Toplevel.ignored (Position.set_range (Command.range toks)), false) - | _ => (Toplevel.malformed proper_range "Exactly one command expected", true)) - handle ERROR msg => (Toplevel.malformed proper_range msg, true) - end; - -fun read_element outer_syntax init (Thy_Syntax.Element (head, opt_proof)) = - let - val read = read_span outer_syntax o Thy_Syntax.span_content; - val (tr, proper_head) = read head |>> Toplevel.modify_init init; - val proof_trs = - (case opt_proof of - NONE => [] - | SOME (a, b) => map read (maps Thy_Syntax.flat_element a @ [b]) |> filter #2 |> map #1); - in - if proper_head andalso - not (Keyword.is_schematic_goal (Toplevel.name_of tr)) then [(tr, proof_trs)] - else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs) + Toplevel.malformed pos "Illegal control command" + else tr + | [] => Toplevel.ignored (Position.set_range (Command.range toks)) + | _ => Toplevel.malformed proper_range "Exactly one command expected") + handle ERROR msg => Toplevel.malformed proper_range msg end; end; diff -r c68c1b89a0f1 -r fcc4b89a600d src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Sun Feb 24 14:14:07 2013 +0100 +++ b/src/Pure/Isar/toplevel.ML Sun Feb 24 17:29:55 2013 +0100 @@ -51,6 +51,7 @@ val keep': (bool -> state -> unit) -> transition -> transition val imperative: (unit -> unit) -> transition -> transition val ignored: Position.T -> transition + val is_ignored: transition -> bool val malformed: Position.T -> string -> transition val is_malformed: transition -> bool val generic_theory: (generic_theory -> generic_theory) -> transition -> transition @@ -414,6 +415,7 @@ fun imperative f = keep (fn _ => f ()); fun ignored pos = empty |> name "" |> position pos |> imperative I; +fun is_ignored tr = name_of tr = ""; val malformed_name = ""; fun malformed pos msg = diff -r c68c1b89a0f1 -r fcc4b89a600d src/Pure/PIDE/document.ML --- a/src/Pure/PIDE/document.ML Sun Feb 24 14:14:07 2013 +0100 +++ b/src/Pure/PIDE/document.ML Sun Feb 24 17:29:55 2013 +0100 @@ -268,9 +268,8 @@ val id_string = print_id id; val span = Lazy.lazy (fn () => Position.setmp_thread_data (Position.id_only id_string) - (fn () => - Thy_Syntax.parse_tokens - (#1 (Outer_Syntax.get_syntax ())) (Position.id id_string) text) ()); + (fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id_string) text) + ()); val _ = Position.setmp_thread_data (Position.id_only id_string) (fn () => Output.status (Markup.markup_only Markup.accepted)) (); @@ -453,7 +452,7 @@ (fn () => let val tr = - #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span) + Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span |> modify_init |> Toplevel.put_id exec_id'_string; val cmts = Outer_Syntax.span_cmts span; diff -r c68c1b89a0f1 -r fcc4b89a600d src/Pure/Thy/thy_load.ML --- a/src/Pure/Thy/thy_load.ML Sun Feb 24 14:14:07 2013 +0100 +++ b/src/Pure/Thy/thy_load.ML Sun Feb 24 17:29:55 2013 +0100 @@ -218,18 +218,30 @@ let val immediate = not (Goal.future_enabled ()); - fun put_timing tr = Toplevel.put_timing (last_timing tr) tr; - fun put_timings (tr, trs) = (put_timing tr, map put_timing trs); + fun prepare_span span = + Thy_Syntax.span_content span + |> Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) + |> Toplevel.modify_init init + |> (fn tr => Toplevel.put_timing (last_timing tr) tr); - fun proof_result (tr, trs) (st, _) = + fun element_result span_elem (st, _) = let - val (result, st') = Toplevel.proof_result immediate (tr, trs) st; - val pos' = Toplevel.pos_of (List.last (tr :: trs)); - in (result, (st', pos')) end; + val tr_elem = Thy_Syntax.map_element prepare_span span_elem; + val Thy_Syntax.Element (tr, opt_proof) = tr_elem; + val proof_trs = + (case opt_proof of + NONE => [] + | SOME (a, b) => (maps Thy_Syntax.flat_element a @ [b]) |> filter_out Toplevel.is_ignored); - fun element_result elem x = - fold_map (proof_result o put_timings) - (Outer_Syntax.read_element (#2 (Outer_Syntax.get_syntax ())) init elem) x; + val elems = + if Toplevel.is_ignored tr then map (rpair []) proof_trs + else if Keyword.is_schematic_goal (Toplevel.name_of tr) + then map (rpair []) (tr :: proof_trs) + else [(tr, proof_trs)]; + + val (results, st') = fold_map (Toplevel.proof_result immediate) elems st; + val pos' = Toplevel.pos_of (Thy_Syntax.last_element tr_elem); + in (results, (st', pos')) end; val (results, (end_state, end_pos)) = fold_map element_result elements (Toplevel.toplevel, Position.none); diff -r c68c1b89a0f1 -r fcc4b89a600d src/Pure/Thy/thy_syntax.ML --- a/src/Pure/Thy/thy_syntax.ML Sun Feb 24 14:14:07 2013 +0100 +++ b/src/Pure/Thy/thy_syntax.ML Sun Feb 24 17:29:55 2013 +0100 @@ -18,6 +18,7 @@ datatype 'a element = Element of 'a * ('a element list * 'a) option val map_element: ('a -> 'b) -> 'a element -> 'b element val flat_element: 'a element -> 'a list + val last_element: 'a element -> 'a val parse_elements: span list -> span element list end; @@ -148,6 +149,9 @@ fun flat_element (Element (a, NONE)) = [a] | flat_element (Element (a, SOME (elems, b))) = a :: maps flat_element elems @ [b]; +fun last_element (Element (a, NONE)) = a + | last_element (Element (_, SOME (_, b))) = b; + (* scanning spans *)