more robust treatment of symbolic indentifiers (which may contain colons);
authorwenzelm
Sat Oct 16 21:23:34 2010 +0100 (2010-10-16)
changeset 398585be7a57c3b4e
parent 39857 ea93e088398d
child 39859 381e16bb5f46
more robust treatment of symbolic indentifiers (which may contain colons);
doc-src/antiquote_setup.ML
     1.1 --- a/doc-src/antiquote_setup.ML	Sat Oct 16 20:27:35 2010 +0100
     1.2 +++ b/doc-src/antiquote_setup.ML	Sat Oct 16 21:23:34 2010 +0100
     1.3 @@ -44,13 +44,13 @@
     1.4  local
     1.5  
     1.6  fun ml_val (txt1, "") = "fn _ => (" ^ txt1 ^ ");"
     1.7 -  | ml_val (txt1, txt2) = "fn _ => (" ^ txt1 ^ ": " ^ txt2 ^ ");";
     1.8 +  | ml_val (txt1, txt2) = "fn _ => (" ^ txt1 ^ " : " ^ txt2 ^ ");";
     1.9  
    1.10  fun ml_type (txt1, "") = "val _ = NONE : (" ^ txt1 ^ ") option;"
    1.11    | ml_type (txt1, txt2) = "val _ = [NONE : (" ^ txt1 ^ ") option, NONE : (" ^ txt2 ^ ") option];";
    1.12  
    1.13 -fun ml_exn (txt1, "") = "fn _ => (" ^ txt1 ^ ": exn);"
    1.14 -  | ml_exn (txt1, txt2) = "fn _ => (" ^ txt1 ^ ": " ^ txt2 ^ " -> exn);";
    1.15 +fun ml_exn (txt1, "") = "fn _ => (" ^ txt1 ^ " : exn);"
    1.16 +  | ml_exn (txt1, txt2) = "fn _ => (" ^ txt1 ^ " : " ^ txt2 ^ " -> exn);";
    1.17  
    1.18  fun ml_structure (txt, _) = "functor XXX() = struct structure XX = " ^ txt ^ " end;";
    1.19  
    1.20 @@ -64,7 +64,8 @@
    1.21          if txt2 = "" then txt1
    1.22          else if kind = "type" then txt1 ^ " = " ^ txt2
    1.23          else if kind = "exception" then txt1 ^ " of " ^ txt2
    1.24 -        else txt1 ^ ": " ^ txt2;
    1.25 +        else if Syntax.is_identifier (Long_Name.base_name txt1) then txt1 ^ ": " ^ txt2
    1.26 +        else txt1 ^ " : " ^ txt2;
    1.27        val txt' = if kind = "" then txt else kind ^ " " ^ txt;
    1.28        val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none (ml (txt1, txt2));  (* ML_Lex.read (!?) *)
    1.29        val kind' = if kind = "" then "ML" else "ML " ^ kind;