src/Pure/Isar/outer_syntax.ML
changeset 9132 52286129faa5
parent 9056 8f78b2aea39e
child 9213 2651a4db8883
     1.1 --- a/src/Pure/Isar/outer_syntax.ML	Sun Jun 25 23:52:59 2000 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.ML	Sun Jun 25 23:54:13 2000 +0200
     1.3 @@ -46,11 +46,7 @@
     1.4    type parser
     1.5    val command: string -> string -> string ->
     1.6      (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
     1.7 -  val markup_command: string -> string -> string ->
     1.8 -    (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
     1.9 -  val markup_env_command: string -> string -> string ->
    1.10 -    (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
    1.11 -  val verbatim_command: string -> string -> string ->
    1.12 +  val markup_command: IsarOutput.markup -> string -> string -> string ->
    1.13      (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
    1.14    val improper_command: string -> string -> string ->
    1.15      (token list -> (Toplevel.transition -> Toplevel.transition) * token list) -> parser
    1.16 @@ -60,7 +56,6 @@
    1.17    val print_help: Toplevel.transition -> Toplevel.transition
    1.18    val add_keywords: string list -> unit
    1.19    val add_parsers: parser list -> unit
    1.20 -  val theory_header: token list -> (string * string list * (string * bool) list) * token list
    1.21    val deps_thy: string -> bool -> Path.T -> string list * Path.T list
    1.22    val load_thy: string -> bool -> bool -> Path.T -> unit
    1.23    val isar: bool -> bool -> Toplevel.isar
    1.24 @@ -111,10 +106,8 @@
    1.25  type token = T.token;
    1.26  type parser_fn = token list -> (Toplevel.transition -> Toplevel.transition) * token list;
    1.27  
    1.28 -datatype markup_kind = Markup | MarkupEnv | Verbatim;
    1.29 -
    1.30  datatype parser =
    1.31 -  Parser of string * (string * string * markup_kind option) * bool * parser_fn;
    1.32 +  Parser of string * (string * string * IsarOutput.markup option) * bool * parser_fn;
    1.33  
    1.34  fun parser int_only markup name comment kind parse =
    1.35    Parser (name, (comment, kind, markup), int_only, parse);
    1.36 @@ -130,12 +123,12 @@
    1.37    | None => sys_error ("no parser for outer syntax command " ^ quote name));
    1.38  
    1.39  fun terminator false = Scan.succeed ()
    1.40 -  | terminator true = P.group "end of input" (Scan.option P.sync -- P.$$$ ";" >> K ());
    1.41 +  | terminator true = P.group "end of input" (Scan.option P.sync -- P.semicolon >> K ());
    1.42  
    1.43  in
    1.44  
    1.45  fun command term cmd =
    1.46 -  P.$$$ ";" >> K None ||
    1.47 +  P.semicolon >> K None ||
    1.48    P.sync >> K None ||
    1.49    (P.position P.command :-- command_body cmd) --| terminator term
    1.50      >> (fn ((name, pos), (int_only, f)) =>
    1.51 @@ -146,14 +139,15 @@
    1.52  
    1.53  
    1.54  
    1.55 -(** global syntax state **)
    1.56 +(** global outer syntax **)
    1.57  
    1.58  local
    1.59  
    1.60  val global_lexicons = ref (Scan.empty_lexicon, Scan.empty_lexicon);
    1.61  val global_parsers =
    1.62 -  ref (Symtab.empty: (((string * string) * (bool * parser_fn)) * markup_kind option) Symtab.table);
    1.63 -val global_markups = ref ([]: (string * markup_kind) list);
    1.64 +  ref (Symtab.empty: (((string * string) * (bool * parser_fn)) * IsarOutput.markup option)
    1.65 +    Symtab.table);
    1.66 +val global_markups = ref ([]: (string * IsarOutput.markup) list);
    1.67  
    1.68  fun change_lexicons f =
    1.69    let val lexs = f (! global_lexicons) in
    1.70 @@ -166,12 +160,12 @@
    1.71    | get_markup (ms, _) = ms;
    1.72  
    1.73  fun make_markups () = global_markups := Symtab.foldl get_markup ([], ! global_parsers);
    1.74 -fun change_parsers f = (global_parsers := f (! global_parsers); make_markups ());
    1.75 +fun change_parsers f = (Library.change global_parsers f; make_markups ());
    1.76  
    1.77  in
    1.78  
    1.79  
    1.80 -(* get current syntax *)
    1.81 +(* access current syntax *)
    1.82  
    1.83  (*Note: the syntax for files is statically determined at the very
    1.84    beginning; for interactive processing it may change dynamically.*)
    1.85 @@ -180,8 +174,9 @@
    1.86  fun get_parsers () = ! global_parsers;
    1.87  fun get_parser () = apsome (#2 o #1) o curry Symtab.lookup (! global_parsers);
    1.88  
    1.89 -fun lookup_markup name = assoc (! global_markups, name);
    1.90 -fun is_markup kind name = (case lookup_markup name of Some k => k = kind | None => false);
    1.91 +fun is_markup kind name =
    1.92 +  (case assoc (! global_markups, name) of Some k => k = kind | None => false);
    1.93 +fun markup kind = Scan.one (T.is_kind T.Command andf is_markup kind o T.val_of);
    1.94  
    1.95  
    1.96  (* augment syntax *)
    1.97 @@ -234,109 +229,50 @@
    1.98  
    1.99  
   1.100  
   1.101 -(** read theory **)
   1.102 -
   1.103 -(* special keywords *)
   1.104 -
   1.105 -val headerN = "header";
   1.106 -val theoryN = "theory";
   1.107 -
   1.108 -val theory_keyword = P.$$$ theoryN;
   1.109 -val header_keyword = P.$$$ headerN;
   1.110 -val semicolon = P.$$$ ";";
   1.111 -
   1.112 -
   1.113 -(* sources *)
   1.114 -
   1.115 -local
   1.116 +(** toplevel parsing **)
   1.117  
   1.118 -val no_terminator =
   1.119 -  Scan.unless semicolon (Scan.one (T.not_sync andf T.not_eof));
   1.120 -
   1.121 -val recover = Scan.prompt "recover# " (Scan.repeat no_terminator);
   1.122 -
   1.123 -in
   1.124 -
   1.125 -fun source term do_recover cmd src =
   1.126 -  src
   1.127 -  |> Source.source T.stopper
   1.128 -    (Scan.bulk (fn xs => P.!!! (command term (cmd ())) xs))
   1.129 -    (if do_recover then Some recover else None)
   1.130 -  |> Source.mapfilter I;
   1.131 -
   1.132 -end;
   1.133 +(* basic sources *)
   1.134  
   1.135  fun token_source (src, pos) =
   1.136    src
   1.137    |> Symbol.source false
   1.138    |> T.source false (K (get_lexicons ())) pos;
   1.139  
   1.140 -fun filter_proper src =
   1.141 -  src
   1.142 -  |> Source.filter T.is_proper;
   1.143 -
   1.144 -
   1.145 -(* scan header *)
   1.146 -
   1.147 -fun scan_header get_lex scan (src, pos) =
   1.148 -  src
   1.149 -  |> Symbol.source false
   1.150 -  |> T.source false (fn () => (get_lex (), Scan.empty_lexicon)) pos
   1.151 -  |> filter_proper
   1.152 -  |> Source.source T.stopper (Scan.single scan) None
   1.153 -  |> (fst o the o Source.get_single);
   1.154 +fun toplevel_source term do_recover cmd src =
   1.155 +  let
   1.156 +    val no_terminator =
   1.157 +      Scan.unless P.semicolon (Scan.one (T.not_sync andf T.not_eof));
   1.158 +    val recover = Scan.prompt "recover# " (Scan.repeat no_terminator);
   1.159 +  in
   1.160 +    src
   1.161 +    |> Source.source T.stopper
   1.162 +      (Scan.bulk (fn xs => P.!!! (command term (cmd ())) xs))
   1.163 +      (if do_recover then Some recover else None)
   1.164 +    |> Source.mapfilter I
   1.165 +  end;
   1.166  
   1.167  
   1.168 -(* detect new/old header *)
   1.169 -
   1.170 -local
   1.171 +(* interactive source of toplevel transformers *)
   1.172  
   1.173 -val check_header_lexicon = Scan.make_lexicon [Symbol.explode headerN, Symbol.explode theoryN];
   1.174 -val check_header = Scan.option (header_keyword || theory_keyword);
   1.175 -
   1.176 -in
   1.177 -
   1.178 -fun is_old_theory src = is_none (scan_header (K check_header_lexicon) check_header src);
   1.179 -
   1.180 -end;
   1.181 +fun isar term no_pos =
   1.182 +  Source.tty
   1.183 +  |> Symbol.source true
   1.184 +  |> T.source true get_lexicons
   1.185 +    (if no_pos then Position.none else Position.line_name 1 "stdin")
   1.186 +  |> T.source_proper
   1.187 +  |> toplevel_source term true get_parser;
   1.188  
   1.189  
   1.190 -(* deps_thy --- inspect theory header *)
   1.191 -
   1.192 -local
   1.193 -
   1.194 -val header_lexicon =
   1.195 -  Scan.make_lexicon (map Symbol.explode ["(", ")", "+", ":", ";", "=", "files", headerN, theoryN]);
   1.196 -
   1.197 -val file_name =
   1.198 -  (P.$$$ "(" |-- P.!!! (P.name --| P.$$$ ")")) >> rpair false || P.name >> rpair true;
   1.199 -
   1.200 -in
   1.201  
   1.202 -val theory_header =
   1.203 -  (P.name -- (P.$$$ "=" |-- P.enum1 "+" P.name) --
   1.204 -    Scan.optional (P.$$$ "files" |-- P.!!! (Scan.repeat1 file_name)) [] --|  P.$$$ ":")
   1.205 -  >> (fn ((A, Bs), files) => (A, Bs, files));
   1.206 +(** read theory **)
   1.207  
   1.208 -val new_header =
   1.209 -  header_keyword |-- (P.!!! (P.text -- Scan.option semicolon -- theory_keyword |-- theory_header))
   1.210 -    || theory_keyword |-- P.!!! theory_header;
   1.211 -
   1.212 -val old_header =
   1.213 -  P.!!! (P.group "theory header"
   1.214 -    (P.name -- (P.$$$ "=" |-- P.name -- Scan.repeat (P.$$$ "+" |-- P.name))))
   1.215 -  >> (fn (A, (B, Bs)) => (A, B :: Bs, []: (string * bool) list));
   1.216 +(* deps_thy *)
   1.217  
   1.218  fun deps_thy name ml path =
   1.219    let
   1.220      val src = Source.of_string (File.read path);
   1.221      val pos = Path.position path;
   1.222 -    val (name', parents, files) =
   1.223 -      (*unfortunately, old-style headers dynamically depend on the current lexicon*)
   1.224 -      if is_old_theory (src, pos) then
   1.225 -        scan_header ThySyn.get_lexicon (Scan.error old_header) (src, pos)
   1.226 -      else scan_header (K header_lexicon) (Scan.error new_header) (src, pos);
   1.227 -
   1.228 +    val (name', parents, files) = ThyHeader.scan (src, pos);
   1.229      val ml_path = ThyLoad.ml_path name;
   1.230      val ml_file = if ml andalso is_some (ThyLoad.check_file ml_path) then [ml_path] else [];
   1.231    in
   1.232 @@ -346,67 +282,8 @@
   1.233      else (parents, map (Path.unpack o #1) files @ ml_file)
   1.234    end;
   1.235  
   1.236 -end;
   1.237  
   1.238 -
   1.239 -(* present theory source *)
   1.240 -
   1.241 -local
   1.242 -
   1.243 -val is_improper = not o (T.is_proper orf T.is_begin_ignore orf T.is_end_ignore);
   1.244 -val improper = Scan.any is_improper;
   1.245 -
   1.246 -val improper_keep_indent = Scan.repeat
   1.247 -  (Scan.unless (Scan.one T.is_indent -- Scan.one T.is_proper) (Scan.one is_improper));
   1.248 -
   1.249 -val improper_end =
   1.250 -  (improper -- semicolon) |-- improper_keep_indent ||
   1.251 -  improper_keep_indent;
   1.252 -
   1.253 -
   1.254 -val ignore =
   1.255 -  Scan.depend (fn d => Scan.one T.is_begin_ignore >> pair (d + 1)) ||
   1.256 -  Scan.depend (fn 0 => Scan.fail | d => Scan.one T.is_end_ignore >> pair (d - 1)) ||
   1.257 -  Scan.lift (Scan.one (OuterLex.not_eof andf (not o OuterLex.is_end_ignore)));
   1.258 -
   1.259 -val opt_newline = Scan.option (Scan.one T.is_newline);
   1.260 -
   1.261 -val ignore_stuff =
   1.262 -  opt_newline -- Scan.one T.is_begin_ignore --
   1.263 -    P.!!!! (Scan.pass 0 (Scan.repeat ignore) -- Scan.one T.is_end_ignore -- opt_newline);
   1.264 -
   1.265 -fun markup_kind k = Scan.one (T.is_kind T.Command andf is_markup k o T.val_of);
   1.266 -
   1.267 -val markup = markup_kind Markup >> T.val_of;
   1.268 -val markup_env = markup_kind MarkupEnv >> T.val_of;
   1.269 -val verbatim = markup_kind Verbatim;
   1.270 -
   1.271 -val present_token =
   1.272 -  ignore_stuff >> K None ||
   1.273 -  (improper |-- markup -- P.!!!! (improper |-- P.text --| improper_end) >> Present.markup_token ||
   1.274 -    improper |-- markup_env -- P.!!!! (improper |-- P.text --| improper_end) >> Present.markup_env_token ||
   1.275 -    (P.$$$ "--" >> K "cmt") -- P.!!!! (improper |-- P.text) >> Present.markup_token ||
   1.276 -    (improper -- verbatim) |-- P.!!!! (improper |-- P.text --| improper_end)
   1.277 -      >> Present.verbatim_token ||
   1.278 -    Scan.one T.not_eof >> Present.basic_token) >> Some;
   1.279 -
   1.280 -in
   1.281 -
   1.282 -(*note: lazy evaluation ahead*)
   1.283 -
   1.284 -fun present_toks text pos () =
   1.285 -  token_source (Source.of_list (Library.untabify text), pos)
   1.286 -  |> Source.source T.stopper (Scan.bulk (Scan.error present_token)) None
   1.287 -  |> Source.mapfilter I
   1.288 -  |> Source.exhaust;
   1.289 -
   1.290 -fun present_text text () =
   1.291 -  Source.exhaust (Symbol.source false (Source.of_list (Library.untabify text)));
   1.292 -
   1.293 -end;
   1.294 -
   1.295 -
   1.296 -(* load_thy --- read text (including header) *)
   1.297 +(* load_thy *)
   1.298  
   1.299  local
   1.300  
   1.301 @@ -417,28 +294,33 @@
   1.302      val tr_name = if time then "time_use" else "use";
   1.303    in
   1.304      if is_none (ThyLoad.check_file path) then ()
   1.305 -    else Toplevel.excursion_error [Toplevel.empty |> Toplevel.name tr_name |> tr]
   1.306 +    else Toplevel.excursion [Toplevel.empty |> Toplevel.name tr_name |> tr]
   1.307    end;
   1.308  
   1.309 -fun parse_thy src_pos =
   1.310 -  src_pos
   1.311 -  |> token_source
   1.312 -  |> filter_proper
   1.313 -  |> source false false (K (get_parser ()))
   1.314 +fun parse_thy src =
   1.315 +  src
   1.316 +  |> T.source_proper
   1.317 +  |> toplevel_source false false (K (get_parser ()))
   1.318    |> Source.exhaust;
   1.319  
   1.320  fun run_thy name path =
   1.321    let
   1.322 -    val text = explode (File.read path);
   1.323 -    val src = Source.of_list text;
   1.324      val pos = Path.position path;
   1.325 +    val text = Library.untabify (explode (File.read path));
   1.326 +    val text_src = Source.of_list text;
   1.327 +    fun present_text () = Source.exhaust (Symbol.source false text_src);
   1.328    in
   1.329      Present.init_theory name;
   1.330 -    Present.verbatim_source name (present_text text);
   1.331 -    if is_old_theory (src, pos) then (ThySyn.load_thy name text;
   1.332 -      Present.old_symbol_source name (present_text text))   (*note: text presented twice!*)
   1.333 -    else (Toplevel.excursion_error (parse_thy (src, pos));
   1.334 -      Present.token_source name (present_toks text pos))
   1.335 +    Present.verbatim_source name present_text;
   1.336 +    if ThyHeader.is_old (text_src, pos) then (ThySyn.load_thy name text;
   1.337 +      Present.old_symbol_source name present_text)   (*note: text presented twice*)
   1.338 +    else
   1.339 +      let
   1.340 +        val tok_src = Source.exhausted (token_source (text_src, pos));
   1.341 +        val out = Toplevel.excursion_result
   1.342 +          (IsarOutput.parse_thy markup (#1 (get_lexicons ()))
   1.343 +            (parse_thy tok_src) tok_src);
   1.344 +      in Present.theory_output name (Buffer.content out) end
   1.345    end;
   1.346  
   1.347  in
   1.348 @@ -456,17 +338,6 @@
   1.349  end;
   1.350  
   1.351  
   1.352 -(* interactive source of state transformers *)
   1.353 -
   1.354 -fun isar term no_pos =
   1.355 -  Source.tty
   1.356 -  |> Symbol.source true
   1.357 -  |> T.source true get_lexicons
   1.358 -    (if no_pos then Position.none else Position.line_name 1 "stdin")
   1.359 -  |> filter_proper
   1.360 -  |> source term true get_parser;
   1.361 -
   1.362 -
   1.363  
   1.364  (** the read-eval-print loop **)
   1.365  
   1.366 @@ -496,9 +367,7 @@
   1.367  
   1.368  (*final declarations of this structure!*)
   1.369  val command = parser false None;
   1.370 -val markup_command = parser false (Some Markup);
   1.371 -val markup_env_command = parser false (Some MarkupEnv);
   1.372 -val verbatim_command = parser false (Some Verbatim);
   1.373 +val markup_command = parser false o Some;
   1.374  val improper_command = parser true None;
   1.375  
   1.376