src/Pure/Thy/thy_output.ML
changeset 36950 75b8f26f2f07
parent 36745 403585a89772
child 36959 f5417836dbea
     1.1 --- a/src/Pure/Thy/thy_output.ML	Sat May 15 22:24:25 2010 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Sat May 15 23:16:32 2010 +0200
     1.3 @@ -37,7 +37,6 @@
     1.4  struct
     1.5  
     1.6  structure T = OuterLex;
     1.7 -structure P = OuterParse;
     1.8  
     1.9  
    1.10  (** global options **)
    1.11 @@ -132,12 +131,16 @@
    1.12  
    1.13  local
    1.14  
    1.15 -val property = P.xname -- Scan.optional (P.$$$ "=" |-- P.!!! P.xname) "";
    1.16 -val properties = Scan.optional (P.$$$ "[" |-- P.!!! (P.enum "," property --| P.$$$ "]")) [];
    1.17 +val property =
    1.18 +  Parse.xname -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.xname) "";
    1.19 +
    1.20 +val properties =
    1.21 +  Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.enum "," property --| Parse.$$$ "]")) [];
    1.22  
    1.23  in
    1.24  
    1.25 -val antiq = P.!!! (P.position P.xname -- properties -- Args.parse --| Scan.ahead P.eof)
    1.26 +val antiq =
    1.27 +  Parse.!!! (Parse.position Parse.xname -- properties -- Args.parse --| Scan.ahead Parse.eof)
    1.28    >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos)));
    1.29  
    1.30  end;
    1.31 @@ -249,7 +252,7 @@
    1.32      val Span ((cmd_name, cmd_pos, cmd_tags), srcs, span_newline) = span;
    1.33  
    1.34      val (tag, tags) = tag_stack;
    1.35 -    val tag' = try hd (fold OuterKeyword.update_tags cmd_tags (the_list tag));
    1.36 +    val tag' = try hd (fold Keyword.update_tags cmd_tags (the_list tag));
    1.37  
    1.38      val active_tag' =
    1.39        if is_some tag' then tag'
    1.40 @@ -316,11 +319,11 @@
    1.41      (if d = 0 then Scan.fail_with (K "Bad nesting of meta-comments") else opt_newline)
    1.42      >> pair (d - 1));
    1.43  
    1.44 -val tag = (improper -- P.$$$ "%" -- improper) |-- P.!!! (P.tag_name --| blank_end);
    1.45 +val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (Parse.tag_name --| blank_end);
    1.46  
    1.47  val locale =
    1.48 -  Scan.option ((P.$$$ "(" -- improper -- P.$$$ "in") |--
    1.49 -    P.!!! (improper |-- P.xname --| (improper -- P.$$$ ")")));
    1.50 +  Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |--
    1.51 +    Parse.!!! (improper |-- Parse.xname --| (improper -- Parse.$$$ ")")));
    1.52  
    1.53  in
    1.54  
    1.55 @@ -332,26 +335,27 @@
    1.56        >> (fn d => (NONE, (NoToken, ("", d))));
    1.57  
    1.58      fun markup mark mk flag = Scan.peek (fn d =>
    1.59 -      improper |-- P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.content_of)) --
    1.60 +      improper |--
    1.61 +        Parse.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.content_of)) --
    1.62        Scan.repeat tag --
    1.63 -      P.!!!! ((improper -- locale -- improper) |-- P.doc_source --| improper_end)
    1.64 +      Parse.!!!! ((improper -- locale -- improper) |-- Parse.doc_source --| improper_end)
    1.65        >> (fn (((tok, pos), tags), txt) =>
    1.66          let val name = T.content_of tok
    1.67          in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end));
    1.68  
    1.69      val command = Scan.peek (fn d =>
    1.70 -      P.position (Scan.one (T.is_kind T.Command)) --
    1.71 +      Parse.position (Scan.one (T.is_kind T.Command)) --
    1.72        Scan.repeat tag
    1.73        >> (fn ((tok, pos), tags) =>
    1.74          let val name = T.content_of tok
    1.75          in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
    1.76  
    1.77      val cmt = Scan.peek (fn d =>
    1.78 -      P.$$$ "--" |-- P.!!!! (improper |-- P.doc_source)
    1.79 +      Parse.$$$ "--" |-- Parse.!!!! (improper |-- Parse.doc_source)
    1.80        >> (fn txt => (NONE, (MarkupToken ("cmt", txt), ("", d)))));
    1.81  
    1.82      val other = Scan.peek (fn d =>
    1.83 -       P.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d)))));
    1.84 +       Parse.not_eof >> (fn tok => (NONE, (BasicToken tok, ("", d)))));
    1.85  
    1.86      val token =
    1.87        ignored ||
    1.88 @@ -565,7 +569,7 @@
    1.89  
    1.90  (* embedded lemma *)
    1.91  
    1.92 -val _ = OuterKeyword.keyword "by";
    1.93 +val _ = Keyword.keyword "by";
    1.94  
    1.95  val _ = antiquotation "lemma"
    1.96    (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))