simplified;
authorwenzelm
Tue Oct 05 21:18:54 1999 +0200 (1999-10-05)
changeset 7746b52c1a632e6a
parent 7745 131005d3a62d
child 7747 ca4e3b75345a
simplified;
header command;
src/Pure/Isar/outer_syntax.ML
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Tue Oct 05 21:18:13 1999 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Tue Oct 05 21:18:54 1999 +0200
     1.3 @@ -206,10 +206,14 @@
     1.4  
     1.5  (** read theory **)
     1.6  
     1.7 -(* theory keyword *)
     1.8 +(* special keywords *)
     1.9  
    1.10 +val headerN = "header";
    1.11  val theoryN = "theory";
    1.12 +
    1.13  val theory_keyword = OuterParse.$$$ theoryN;
    1.14 +val header_keyword = OuterParse.$$$ headerN;
    1.15 +val semicolon = P.$$$ ";";
    1.16  
    1.17  
    1.18  (* sources *)
    1.19 @@ -217,7 +221,7 @@
    1.20  local
    1.21  
    1.22  val no_terminator =
    1.23 -  Scan.unless (P.$$$ ";") (Scan.one (OuterLex.not_sync andf OuterLex.not_eof));
    1.24 +  Scan.unless semicolon (Scan.one (OuterLex.not_sync andf OuterLex.not_eof));
    1.25  
    1.26  val recover = Scan.prompt "recover# " (Scan.repeat no_terminator);
    1.27  
    1.28 @@ -242,7 +246,7 @@
    1.29    |> Source.filter OuterLex.is_proper;
    1.30  
    1.31  
    1.32 -(* detect header *)
    1.33 +(* scan header *)
    1.34  
    1.35  fun scan_header get_lex scan (src, pos) =
    1.36    src
    1.37 @@ -252,46 +256,54 @@
    1.38    |> Source.source OuterLex.stopper (Scan.single scan) None
    1.39    |> (fst o the o Source.get_single);
    1.40  
    1.41 -val check_header_lexicon = Scan.make_lexicon [Symbol.explode theoryN];
    1.42 +
    1.43 +(* detect new/old header *)
    1.44 +
    1.45 +local
    1.46  
    1.47 -fun is_old_theory src =
    1.48 -  is_none (scan_header (K check_header_lexicon) (Scan.option theory_keyword) src);
    1.49 +val check_header_lexicon = Scan.make_lexicon [Symbol.explode headerN, Symbol.explode theoryN];
    1.50 +val check_header = Scan.option (header_keyword || theory_keyword);
    1.51 +
    1.52 +in
    1.53 +
    1.54 +fun is_old_theory src = is_none (scan_header (K check_header_lexicon) check_header src);
    1.55 +
    1.56 +end;
    1.57  
    1.58  
    1.59  (* deps_thy --- inspect theory header *)
    1.60  
    1.61 +local
    1.62 +
    1.63  val header_lexicon =
    1.64 -  Scan.make_lexicon (map Symbol.explode ["(", ")", "+", ":", "=", "files", theoryN]);
    1.65 -
    1.66 -local
    1.67 +  Scan.make_lexicon (map Symbol.explode ["(", ")", "+", ":", ";", "=", "files", headerN, theoryN]);
    1.68  
    1.69  val file_name =
    1.70    (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) >> rpair false || P.name >> rpair true;
    1.71  
    1.72 -val theory_head =
    1.73 +in
    1.74 +
    1.75 +val theory_header =
    1.76    (P.name -- (P.$$$ "=" |-- P.enum1 "+" P.name) --
    1.77 -    Scan.optional (P.$$$ "files" |-- P.!!! (Scan.repeat1 file_name)) [])
    1.78 +    Scan.optional (P.$$$ "files" |-- P.!!! (Scan.repeat1 file_name)) [] --|  P.$$$ ":")
    1.79    >> (fn ((A, Bs), files) => (A, Bs, files));
    1.80  
    1.81 -in
    1.82 -
    1.83 -val theory_header = theory_head --| (Scan.ahead P.eof || P.$$$ ":");
    1.84 -val only_header = theory_keyword |-- theory_head --| Scan.ahead P.eof;
    1.85 -val new_header = theory_keyword |-- P.!!! theory_header;
    1.86 +val new_header =
    1.87 +  header_keyword |-- (P.!!! (P.text -- Scan.option semicolon -- theory_keyword |-- theory_header))
    1.88 +    || theory_keyword |-- P.!!! theory_header;
    1.89  
    1.90  val old_header =
    1.91    P.name -- (P.$$$ "=" |-- P.name -- Scan.repeat (P.$$$ "+" |-- P.name))
    1.92    >> (fn (A, (B, Bs)) => (A, B :: Bs, []: (string * bool) list));
    1.93  
    1.94 -end;
    1.95 -
    1.96  fun deps_thy name path =
    1.97    let
    1.98      val src = Source.of_string (File.read path);
    1.99      val pos = Path.position path;
   1.100      val (name', parents, files) =
   1.101        (*Note: old style headers dynamically depend on the current lexicon :-( *)
   1.102 -      if is_old_theory (src, pos) then scan_header ThySyn.get_lexicon (Scan.error old_header) (src, pos)
   1.103 +      if is_old_theory (src, pos) then
   1.104 +        scan_header ThySyn.get_lexicon (Scan.error old_header) (src, pos)
   1.105        else scan_header (K header_lexicon) (Scan.error new_header) (src, pos);
   1.106  
   1.107      val ml_path = ThyLoad.ml_path name;
   1.108 @@ -302,9 +314,13 @@
   1.109      else (parents, map (Path.unpack o #1) files @ ml_file)
   1.110    end;
   1.111  
   1.112 +end;
   1.113 +
   1.114  
   1.115  (* load_thy --- read text (including header) *)
   1.116  
   1.117 +local
   1.118 +
   1.119  fun try_ml_file name ml time =
   1.120    let
   1.121      val path = ThyLoad.ml_path name;
   1.122 @@ -316,22 +332,11 @@
   1.123    end;
   1.124  
   1.125  fun parse_thy src_pos =
   1.126 -  let
   1.127 -    val lex_src = filter_proper (token_source src_pos);
   1.128 -    val only_head =
   1.129 -      lex_src
   1.130 -      |> Source.source OuterLex.stopper (Scan.single (Scan.option only_header)) None
   1.131 -      |> (fst o the o Source.get_single);
   1.132 -  in
   1.133 -    (case only_head of
   1.134 -      None =>
   1.135 -        lex_src
   1.136 -        |> source false false (K (get_parser ()))
   1.137 -        |> Source.exhaust
   1.138 -    | Some spec =>
   1.139 -        [Toplevel.empty |> Toplevel.name theoryN |> IsarThy.theory spec,
   1.140 -          Toplevel.empty |> Toplevel.name "end" |> Toplevel.exit])
   1.141 -  end;
   1.142 +  src_pos
   1.143 +  |> token_source
   1.144 +  |> filter_proper
   1.145 +  |> source false false (K (get_parser ()))
   1.146 +  |> Source.exhaust;
   1.147  
   1.148  fun run_thy name path =
   1.149    let
   1.150 @@ -350,6 +355,8 @@
   1.151      Present.verbatim_source name present_text
   1.152    end;
   1.153  
   1.154 +in
   1.155 +
   1.156  fun load_thy name ml time path =
   1.157   (if time then
   1.158      timeit (fn () =>
   1.159 @@ -360,6 +367,8 @@
   1.160    Context.context (ThyInfo.get_theory name);
   1.161    try_ml_file name ml time);
   1.162  
   1.163 +end;
   1.164 +
   1.165  
   1.166  (* interactive source of state transformers *)
   1.167