src/Pure/Thy/thy_output.ML
changeset 27809 a1e409db516b
parent 27781 5a82ee34e9fc
child 27874 f0364f1c0ecf
     1.1 --- a/src/Pure/Thy/thy_output.ML	Sat Aug 09 12:28:13 2008 +0200
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Aug 09 22:43:46 2008 +0200
     1.3 @@ -135,7 +135,7 @@
     1.4  
     1.5  in
     1.6  
     1.7 -val antiq = P.!!! (P.position P.xname -- properties -- P.arguments --| Scan.ahead P.eof)
     1.8 +val antiq = P.!!! (P.position P.xname -- properties -- Args.parse --| Scan.ahead P.eof)
     1.9    >> (fn (((x, pos), y), z) => (y, Args.src ((x, z), pos)));
    1.10  
    1.11  end;
    1.12 @@ -332,18 +332,18 @@
    1.13        >> (fn d => (NONE, (NoToken, ("", d))));
    1.14  
    1.15      fun markup mark mk flag = Scan.peek (fn d =>
    1.16 -      improper |-- P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.val_of)) --
    1.17 +      improper |-- P.position (Scan.one (T.is_kind T.Command andf is_markup mark o T.content_of)) --
    1.18        Scan.repeat tag --
    1.19        P.!!!! ((improper -- locale -- improper) |-- P.position P.text --| improper_end)
    1.20        >> (fn (((tok, pos), tags), txt) =>
    1.21 -        let val name = T.val_of tok
    1.22 +        let val name = T.content_of tok
    1.23          in (SOME (name, pos, tags), (mk (name, txt), (flag, d))) end));
    1.24  
    1.25      val command = Scan.peek (fn d =>
    1.26        P.position (Scan.one (T.is_kind T.Command)) --
    1.27        Scan.repeat tag
    1.28        >> (fn ((tok, pos), tags) =>
    1.29 -        let val name = T.val_of tok
    1.30 +        let val name = T.content_of tok
    1.31          in (SOME (name, pos, tags), (BasicToken tok, (Latex.markup_false, d))) end));
    1.32  
    1.33      val cmt = Scan.peek (fn d =>
    1.34 @@ -428,7 +428,7 @@
    1.35  
    1.36  (* basic pretty printing *)
    1.37  
    1.38 -val str_of_source = space_implode " " o map Args.string_of o #2 o #1 o Args.dest_src;
    1.39 +val str_of_source = space_implode " " o map T.unparse o #2 o #1 o Args.dest_src;
    1.40  
    1.41  fun tweak_line s =
    1.42    if ! display then s else Symbol.strip_blanks s;
    1.43 @@ -527,7 +527,7 @@
    1.44    in pretty_term ctxt prop end;
    1.45  
    1.46  val embedded_lemma =
    1.47 -  args (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse_args -- Scan.option Method.parse_args))
    1.48 +  args (Args.prop -- Scan.lift (Args.$$$ "by" |-- Method.parse -- Scan.option Method.parse))
    1.49      (output pretty_lemma o (fn ((a, arg :: _), p) => (Args.src ((a, [arg]), p))) o Args.dest_src);
    1.50  
    1.51  
    1.52 @@ -553,8 +553,8 @@
    1.53    ("prf", args Attrib.thms (output (pretty_prf false))),
    1.54    ("full_prf", args Attrib.thms (output (pretty_prf true))),
    1.55    ("theory", args (Scan.lift Args.name) (output pretty_theory)),
    1.56 -  ("ML", args (Scan.lift (Args.position Args.name)) (output_ml ml_val)),
    1.57 -  ("ML_type", args (Scan.lift (Args.position Args.name)) (output_ml ml_type)),
    1.58 -  ("ML_struct", args (Scan.lift (Args.position Args.name)) (output_ml ml_struct))];
    1.59 +  ("ML", args (Scan.lift (P.position Args.name)) (output_ml ml_val)),
    1.60 +  ("ML_type", args (Scan.lift (P.position Args.name)) (output_ml ml_type)),
    1.61 +  ("ML_struct", args (Scan.lift (P.position Args.name)) (output_ml ml_struct))];
    1.62  
    1.63  end;