simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored;
authorwenzelm
Sun Feb 24 17:29:55 2013 +0100 (2013-02-24)
changeset 51268fcc4b89a600d
parent 51267 c68c1b89a0f1
child 51269 54725c4acdd0
simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored;
eliminated separate Outer_Syntax.read_element;
src/Pure/Isar/outer_syntax.ML
src/Pure/Isar/toplevel.ML
src/Pure/PIDE/document.ML
src/Pure/Thy/thy_load.ML
src/Pure/Thy/thy_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Sun Feb 24 14:14:07 2013 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sun Feb 24 17:29:55 2013 +0100
     1.3 @@ -35,9 +35,7 @@
     1.4    type isar
     1.5    val isar: TextIO.instream -> bool -> isar
     1.6    val span_cmts: Token.T list -> Token.T list
     1.7 -  val read_span: outer_syntax -> Token.T list -> Toplevel.transition * bool
     1.8 -  val read_element: outer_syntax -> (unit -> theory) -> Thy_Syntax.span Thy_Syntax.element ->
     1.9 -    (Toplevel.transition * Toplevel.transition list) list
    1.10 +  val read_span: outer_syntax -> Token.T list -> Toplevel.transition
    1.11  end;
    1.12  
    1.13  structure Outer_Syntax: OUTER_SYNTAX =
    1.14 @@ -319,30 +317,16 @@
    1.15      val (is_malformed, token_reports) = Thy_Syntax.reports_of_tokens toks;
    1.16      val _ = Position.reports_text (token_reports @ maps command_reports toks);
    1.17    in
    1.18 -    if is_malformed then (Toplevel.malformed pos "Malformed command syntax", true)
    1.19 +    if is_malformed then Toplevel.malformed pos "Malformed command syntax"
    1.20      else
    1.21        (case Source.exhaust (toplevel_source false NONE (K commands) (Source.of_list toks)) of
    1.22          [tr] =>
    1.23            if Keyword.is_control (Toplevel.name_of tr) then
    1.24 -            (Toplevel.malformed pos "Illegal control command", true)
    1.25 -          else (tr, true)
    1.26 -      | [] => (Toplevel.ignored (Position.set_range (Command.range toks)), false)
    1.27 -      | _ => (Toplevel.malformed proper_range "Exactly one command expected", true))
    1.28 -      handle ERROR msg => (Toplevel.malformed proper_range msg, true)
    1.29 -  end;
    1.30 -
    1.31 -fun read_element outer_syntax init (Thy_Syntax.Element (head, opt_proof)) =
    1.32 -  let
    1.33 -    val read = read_span outer_syntax o Thy_Syntax.span_content;
    1.34 -    val (tr, proper_head) = read head |>> Toplevel.modify_init init;
    1.35 -    val proof_trs =
    1.36 -      (case opt_proof of
    1.37 -        NONE => []
    1.38 -      | SOME (a, b) => map read (maps Thy_Syntax.flat_element a @ [b]) |> filter #2 |> map #1);
    1.39 -  in
    1.40 -    if proper_head andalso
    1.41 -      not (Keyword.is_schematic_goal (Toplevel.name_of tr)) then [(tr, proof_trs)]
    1.42 -    else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
    1.43 +            Toplevel.malformed pos "Illegal control command"
    1.44 +          else tr
    1.45 +      | [] => Toplevel.ignored (Position.set_range (Command.range toks))
    1.46 +      | _ => Toplevel.malformed proper_range "Exactly one command expected")
    1.47 +      handle ERROR msg => Toplevel.malformed proper_range msg
    1.48    end;
    1.49  
    1.50  end;
     2.1 --- a/src/Pure/Isar/toplevel.ML	Sun Feb 24 14:14:07 2013 +0100
     2.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Feb 24 17:29:55 2013 +0100
     2.3 @@ -51,6 +51,7 @@
     2.4    val keep': (bool -> state -> unit) -> transition -> transition
     2.5    val imperative: (unit -> unit) -> transition -> transition
     2.6    val ignored: Position.T -> transition
     2.7 +  val is_ignored: transition -> bool
     2.8    val malformed: Position.T -> string -> transition
     2.9    val is_malformed: transition -> bool
    2.10    val generic_theory: (generic_theory -> generic_theory) -> transition -> transition
    2.11 @@ -414,6 +415,7 @@
    2.12  fun imperative f = keep (fn _ => f ());
    2.13  
    2.14  fun ignored pos = empty |> name "<ignored>" |> position pos |> imperative I;
    2.15 +fun is_ignored tr = name_of tr = "<ignored>";
    2.16  
    2.17  val malformed_name = "<malformed>";
    2.18  fun malformed pos msg =
     3.1 --- a/src/Pure/PIDE/document.ML	Sun Feb 24 14:14:07 2013 +0100
     3.2 +++ b/src/Pure/PIDE/document.ML	Sun Feb 24 17:29:55 2013 +0100
     3.3 @@ -268,9 +268,8 @@
     3.4        val id_string = print_id id;
     3.5        val span = Lazy.lazy (fn () =>
     3.6          Position.setmp_thread_data (Position.id_only id_string)
     3.7 -          (fn () =>
     3.8 -            Thy_Syntax.parse_tokens
     3.9 -              (#1 (Outer_Syntax.get_syntax ())) (Position.id id_string) text) ());
    3.10 +          (fn () => Thy_Syntax.parse_tokens (Keyword.get_lexicons ()) (Position.id id_string) text)
    3.11 +            ());
    3.12        val _ =
    3.13          Position.setmp_thread_data (Position.id_only id_string)
    3.14            (fn () => Output.status (Markup.markup_only Markup.accepted)) ();
    3.15 @@ -453,7 +452,7 @@
    3.16            (fn () =>
    3.17              let
    3.18                val tr =
    3.19 -                #1 (Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span)
    3.20 +                Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ())) span
    3.21                  |> modify_init
    3.22                  |> Toplevel.put_id exec_id'_string;
    3.23                val cmts = Outer_Syntax.span_cmts span;
     4.1 --- a/src/Pure/Thy/thy_load.ML	Sun Feb 24 14:14:07 2013 +0100
     4.2 +++ b/src/Pure/Thy/thy_load.ML	Sun Feb 24 17:29:55 2013 +0100
     4.3 @@ -218,18 +218,30 @@
     4.4    let
     4.5      val immediate = not (Goal.future_enabled ());
     4.6  
     4.7 -    fun put_timing tr = Toplevel.put_timing (last_timing tr) tr;
     4.8 -    fun put_timings (tr, trs) = (put_timing tr, map put_timing trs);
     4.9 +    fun prepare_span span =
    4.10 +      Thy_Syntax.span_content span
    4.11 +      |> Outer_Syntax.read_span (#2 (Outer_Syntax.get_syntax ()))
    4.12 +      |> Toplevel.modify_init init
    4.13 +      |> (fn tr => Toplevel.put_timing (last_timing tr) tr);
    4.14  
    4.15 -    fun proof_result (tr, trs) (st, _) =
    4.16 +    fun element_result span_elem (st, _) =
    4.17        let
    4.18 -        val (result, st') = Toplevel.proof_result immediate (tr, trs) st;
    4.19 -        val pos' = Toplevel.pos_of (List.last (tr :: trs));
    4.20 -      in (result, (st', pos')) end;
    4.21 +        val tr_elem = Thy_Syntax.map_element prepare_span span_elem;
    4.22 +        val Thy_Syntax.Element (tr, opt_proof) = tr_elem;
    4.23 +        val proof_trs =
    4.24 +          (case opt_proof of
    4.25 +            NONE => []
    4.26 +          | SOME (a, b) => (maps Thy_Syntax.flat_element a @ [b]) |> filter_out Toplevel.is_ignored);
    4.27  
    4.28 -    fun element_result elem x =
    4.29 -      fold_map (proof_result o put_timings)
    4.30 -        (Outer_Syntax.read_element (#2 (Outer_Syntax.get_syntax ())) init elem) x;
    4.31 +        val elems =
    4.32 +          if Toplevel.is_ignored tr then map (rpair []) proof_trs
    4.33 +          else if Keyword.is_schematic_goal (Toplevel.name_of tr)
    4.34 +          then map (rpair []) (tr :: proof_trs)
    4.35 +          else [(tr, proof_trs)];
    4.36 +
    4.37 +        val (results, st') = fold_map (Toplevel.proof_result immediate) elems st;
    4.38 +        val pos' = Toplevel.pos_of (Thy_Syntax.last_element tr_elem);
    4.39 +      in (results, (st', pos')) end;
    4.40  
    4.41      val (results, (end_state, end_pos)) =
    4.42        fold_map element_result elements (Toplevel.toplevel, Position.none);
     5.1 --- a/src/Pure/Thy/thy_syntax.ML	Sun Feb 24 14:14:07 2013 +0100
     5.2 +++ b/src/Pure/Thy/thy_syntax.ML	Sun Feb 24 17:29:55 2013 +0100
     5.3 @@ -18,6 +18,7 @@
     5.4    datatype 'a element = Element of 'a * ('a element list * 'a) option
     5.5    val map_element: ('a -> 'b) -> 'a element -> 'b element
     5.6    val flat_element: 'a element -> 'a list
     5.7 +  val last_element: 'a element -> 'a
     5.8    val parse_elements: span list -> span element list
     5.9  end;
    5.10  
    5.11 @@ -148,6 +149,9 @@
    5.12  fun flat_element (Element (a, NONE)) = [a]
    5.13    | flat_element (Element (a, SOME (elems, b))) = a :: maps flat_element elems @ [b];
    5.14  
    5.15 +fun last_element (Element (a, NONE)) = a
    5.16 +  | last_element (Element (_, SOME (_, b))) = b;
    5.17 +
    5.18  
    5.19  (* scanning spans *)
    5.20