clarified modules;
authorwenzelm
Wed Aug 29 11:44:28 2018 +0200 (13 months ago)
changeset 68839d8251a61cce8
parent 68838 5e013478bced
child 68840 51ab4c78235b
clarified modules;
src/Pure/Isar/toplevel.ML
src/Pure/ROOT.ML
src/Pure/Thy/thy_element.ML
src/Pure/Thy/thy_info.ML
src/Pure/Thy/thy_syntax.ML
     1.1 --- a/src/Pure/Isar/toplevel.ML	Wed Aug 29 07:50:28 2018 +0100
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Aug 29 11:44:28 2018 +0200
     1.3 @@ -86,7 +86,7 @@
     1.4    val reset_proof: state -> state option
     1.5    type result
     1.6    val join_results: result -> (transition * state) list
     1.7 -  val element_result: Keyword.keywords -> transition Thy_Syntax.element -> state -> result * state
     1.8 +  val element_result: Keyword.keywords -> transition Thy_Element.element -> state -> result * state
     1.9  end;
    1.10  
    1.11  structure Toplevel: TOPLEVEL =
    1.12 @@ -669,7 +669,7 @@
    1.13  val put_result = Proof.map_context o Result.put;
    1.14  
    1.15  fun timing_estimate elem =
    1.16 -  let val trs = tl (Thy_Syntax.flat_element elem)
    1.17 +  let val trs = tl (Thy_Element.flat_element elem)
    1.18    in fold (fn tr => fn t => get_timing tr + t) trs Time.zeroTime end;
    1.19  
    1.20  fun future_proofs_enabled estimate st =
    1.21 @@ -693,8 +693,8 @@
    1.22  
    1.23  in
    1.24  
    1.25 -fun element_result keywords (Thy_Syntax.Element (tr, NONE)) st = atom_result keywords tr st
    1.26 -  | element_result keywords (elem as Thy_Syntax.Element (head_tr, SOME element_rest)) st =
    1.27 +fun element_result keywords (Thy_Element.Element (tr, NONE)) st = atom_result keywords tr st
    1.28 +  | element_result keywords (elem as Thy_Element.Element (head_tr, SOME element_rest)) st =
    1.29        let
    1.30          val (head_result, st') = atom_result keywords head_tr st;
    1.31          val (body_elems, end_tr) = element_rest;
    1.32 @@ -703,7 +703,7 @@
    1.33          if not (future_proofs_enabled estimate st')
    1.34          then
    1.35            let
    1.36 -            val proof_trs = maps Thy_Syntax.flat_element body_elems @ [end_tr];
    1.37 +            val proof_trs = maps Thy_Element.flat_element body_elems @ [end_tr];
    1.38              val (proof_results, st'') = fold_map (atom_result keywords) proof_trs st';
    1.39            in (Result_List (head_result :: proof_results), st'') end
    1.40          else
     2.1 --- a/src/Pure/ROOT.ML	Wed Aug 29 07:50:28 2018 +0100
     2.2 +++ b/src/Pure/ROOT.ML	Wed Aug 29 11:44:28 2018 +0200
     2.3 @@ -222,7 +222,7 @@
     2.4  ML_file "Isar/local_theory.ML";
     2.5  ML_file "Isar/entity.ML";
     2.6  ML_file "PIDE/command_span.ML";
     2.7 -ML_file "Thy/thy_syntax.ML";
     2.8 +ML_file "Thy/thy_element.ML";
     2.9  ML_file "Thy/markdown.ML";
    2.10  ML_file "Thy/html.ML";
    2.11  ML_file "Thy/latex.ML";
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/Pure/Thy/thy_element.ML	Wed Aug 29 11:44:28 2018 +0200
     3.3 @@ -0,0 +1,83 @@
     3.4 +(*  Title:      Pure/Thy/thy_element.ML
     3.5 +    Author:     Makarius
     3.6 +
     3.7 +Theory elements: statements with optional proof.
     3.8 +*)
     3.9 +
    3.10 +signature THY_ELEMENT =
    3.11 +sig
    3.12 +  datatype 'a element = Element of 'a * ('a element list * 'a) option
    3.13 +  val atom: 'a -> 'a element
    3.14 +  val map_element: ('a -> 'b) -> 'a element -> 'b element
    3.15 +  val flat_element: 'a element -> 'a list
    3.16 +  val last_element: 'a element -> 'a
    3.17 +  val parse_elements: Keyword.keywords -> Command_Span.span list -> Command_Span.span element list
    3.18 +end;
    3.19 +
    3.20 +structure Thy_Element: THY_ELEMENT =
    3.21 +struct
    3.22 +
    3.23 +(* datatype element: command with optional proof *)
    3.24 +
    3.25 +datatype 'a element = Element of 'a * ('a element list * 'a) option;
    3.26 +
    3.27 +fun element (a, b) = Element (a, SOME b);
    3.28 +fun atom a = Element (a, NONE);
    3.29 +
    3.30 +fun map_element f (Element (a, NONE)) = Element (f a, NONE)
    3.31 +  | map_element f (Element (a, SOME (elems, b))) =
    3.32 +      Element (f a, SOME ((map o map_element) f elems, f b));
    3.33 +
    3.34 +fun flat_element (Element (a, NONE)) = [a]
    3.35 +  | flat_element (Element (a, SOME (elems, b))) = a :: maps flat_element elems @ [b];
    3.36 +
    3.37 +fun last_element (Element (a, NONE)) = a
    3.38 +  | last_element (Element (_, SOME (_, b))) = b;
    3.39 +
    3.40 +
    3.41 +(* scanning spans *)
    3.42 +
    3.43 +val eof = Command_Span.Span (Command_Span.Command_Span ("", Position.none), []);
    3.44 +
    3.45 +fun is_eof (Command_Span.Span (Command_Span.Command_Span ("", _), _)) = true
    3.46 +  | is_eof _ = false;
    3.47 +
    3.48 +val not_eof = not o is_eof;
    3.49 +
    3.50 +val stopper = Scan.stopper (K eof) is_eof;
    3.51 +
    3.52 +
    3.53 +(* parse *)
    3.54 +
    3.55 +local
    3.56 +
    3.57 +fun command_with pred =
    3.58 +  Scan.one
    3.59 +    (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) => pred name | _ => false);
    3.60 +
    3.61 +fun parse_element keywords =
    3.62 +  let
    3.63 +    val proof_atom =
    3.64 +      Scan.one
    3.65 +        (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) =>
    3.66 +              Keyword.is_proof_body keywords name
    3.67 +          | _ => true) >> atom;
    3.68 +    fun proof_element x =
    3.69 +      (command_with (Keyword.is_proof_goal keywords) -- proof_rest >> element || proof_atom) x
    3.70 +    and proof_rest x =
    3.71 +      (Scan.repeat proof_element -- command_with (Keyword.is_qed keywords)) x;
    3.72 +  in
    3.73 +    command_with (Keyword.is_theory_goal keywords) -- proof_rest >> element ||
    3.74 +    Scan.one not_eof >> atom
    3.75 +  end;
    3.76 +
    3.77 +in
    3.78 +
    3.79 +fun parse_elements keywords =
    3.80 +  Source.of_list #>
    3.81 +  Source.source stopper (Scan.bulk (parse_element keywords)) #>
    3.82 +  Source.exhaust;
    3.83 +
    3.84 +end;
    3.85 +
    3.86 +end;
     4.1 --- a/src/Pure/Thy/thy_info.ML	Wed Aug 29 07:50:28 2018 +0100
     4.2 +++ b/src/Pure/Thy/thy_info.ML	Wed Aug 29 11:44:28 2018 +0200
     4.3 @@ -289,9 +289,9 @@
     4.4  
     4.5      fun element_result span_elem (st, _) =
     4.6        let
     4.7 -        val elem = Thy_Syntax.map_element (prepare_span st) span_elem;
     4.8 +        val elem = Thy_Element.map_element (prepare_span st) span_elem;
     4.9          val (results, st') = Toplevel.element_result keywords elem st;
    4.10 -        val pos' = Toplevel.pos_of (Thy_Syntax.last_element elem);
    4.11 +        val pos' = Toplevel.pos_of (Thy_Element.last_element elem);
    4.12        in (results, (st', pos')) end;
    4.13  
    4.14      val (results, (end_state, end_pos)) =
    4.15 @@ -309,7 +309,7 @@
    4.16          (Keyword.add_keywords (#keywords header) Keyword.empty_keywords);
    4.17  
    4.18      val spans = Outer_Syntax.parse_spans (Token.explode keywords text_pos text);
    4.19 -    val elements = Thy_Syntax.parse_elements keywords spans;
    4.20 +    val elements = Thy_Element.parse_elements keywords spans;
    4.21  
    4.22      fun init () =
    4.23        Resources.begin_theory master_dir header parents
     5.1 --- a/src/Pure/Thy/thy_syntax.ML	Wed Aug 29 07:50:28 2018 +0100
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,83 +0,0 @@
     5.4 -(*  Title:      Pure/Thy/thy_syntax.ML
     5.5 -    Author:     Makarius
     5.6 -
     5.7 -Theory syntax elements.
     5.8 -*)
     5.9 -
    5.10 -signature THY_SYNTAX =
    5.11 -sig
    5.12 -  datatype 'a element = Element of 'a * ('a element list * 'a) option
    5.13 -  val atom: 'a -> 'a element
    5.14 -  val map_element: ('a -> 'b) -> 'a element -> 'b element
    5.15 -  val flat_element: 'a element -> 'a list
    5.16 -  val last_element: 'a element -> 'a
    5.17 -  val parse_elements: Keyword.keywords -> Command_Span.span list -> Command_Span.span element list
    5.18 -end;
    5.19 -
    5.20 -structure Thy_Syntax: THY_SYNTAX =
    5.21 -struct
    5.22 -
    5.23 -(* datatype element: command with optional proof *)
    5.24 -
    5.25 -datatype 'a element = Element of 'a * ('a element list * 'a) option;
    5.26 -
    5.27 -fun element (a, b) = Element (a, SOME b);
    5.28 -fun atom a = Element (a, NONE);
    5.29 -
    5.30 -fun map_element f (Element (a, NONE)) = Element (f a, NONE)
    5.31 -  | map_element f (Element (a, SOME (elems, b))) =
    5.32 -      Element (f a, SOME ((map o map_element) f elems, f b));
    5.33 -
    5.34 -fun flat_element (Element (a, NONE)) = [a]
    5.35 -  | flat_element (Element (a, SOME (elems, b))) = a :: maps flat_element elems @ [b];
    5.36 -
    5.37 -fun last_element (Element (a, NONE)) = a
    5.38 -  | last_element (Element (_, SOME (_, b))) = b;
    5.39 -
    5.40 -
    5.41 -(* scanning spans *)
    5.42 -
    5.43 -val eof = Command_Span.Span (Command_Span.Command_Span ("", Position.none), []);
    5.44 -
    5.45 -fun is_eof (Command_Span.Span (Command_Span.Command_Span ("", _), _)) = true
    5.46 -  | is_eof _ = false;
    5.47 -
    5.48 -val not_eof = not o is_eof;
    5.49 -
    5.50 -val stopper = Scan.stopper (K eof) is_eof;
    5.51 -
    5.52 -
    5.53 -(* parse *)
    5.54 -
    5.55 -local
    5.56 -
    5.57 -fun command_with pred =
    5.58 -  Scan.one
    5.59 -    (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) => pred name | _ => false);
    5.60 -
    5.61 -fun parse_element keywords =
    5.62 -  let
    5.63 -    val proof_atom =
    5.64 -      Scan.one
    5.65 -        (fn (Command_Span.Span (Command_Span.Command_Span (name, _), _)) =>
    5.66 -              Keyword.is_proof_body keywords name
    5.67 -          | _ => true) >> atom;
    5.68 -    fun proof_element x =
    5.69 -      (command_with (Keyword.is_proof_goal keywords) -- proof_rest >> element || proof_atom) x
    5.70 -    and proof_rest x =
    5.71 -      (Scan.repeat proof_element -- command_with (Keyword.is_qed keywords)) x;
    5.72 -  in
    5.73 -    command_with (Keyword.is_theory_goal keywords) -- proof_rest >> element ||
    5.74 -    Scan.one not_eof >> atom
    5.75 -  end;
    5.76 -
    5.77 -in
    5.78 -
    5.79 -fun parse_elements keywords =
    5.80 -  Source.of_list #>
    5.81 -  Source.source stopper (Scan.bulk (parse_element keywords)) #>
    5.82 -  Source.exhaust;
    5.83 -
    5.84 -end;
    5.85 -
    5.86 -end;