rename #(FNAME) to #(FILE)

src/combin/combinScript.sml

@@ -20,16 +20,16 @@ val _ = new_theory "combin";
 
 fun def (s,l) p = Q.new_definition_at (DB_dtype.mkloc(s,l,false)) p
 
-val K_DEF = def(#(FNAME),#(LINE))("K_DEF",        `K = \x y. x`);
-val S_DEF = def(#(FNAME),#(LINE))("S_DEF",        `S = \f g x. f x (g x)`);
-val I_DEF = def(#(FNAME),#(LINE))("I_DEF",        `I = S K (K:'a->'a->'a)`);
-val C_DEF = def(#(FNAME),#(LINE))("C_DEF",        `C = \f x y. f y x`);
-val W_DEF = def(#(FNAME),#(LINE))("W_DEF",        `W = \f x. f x x`);
-val o_DEF = def(#(FNAME),#(LINE))("o_DEF", `$o f g = \x. f(g x)`);
+val K_DEF = def(#(FILE),#(LINE))("K_DEF",        `K = \x y. x`);
+val S_DEF = def(#(FILE),#(LINE))("S_DEF",        `S = \f g x. f x (g x)`);
+val I_DEF = def(#(FILE),#(LINE))("I_DEF",        `I = S K (K:'a->'a->'a)`);
+val C_DEF = def(#(FILE),#(LINE))("C_DEF",        `C = \f x y. f y x`);
+val W_DEF = def(#(FILE),#(LINE))("W_DEF",        `W = \f x. f x x`);
+val o_DEF = def(#(FILE),#(LINE))("o_DEF", `$o f g = \x. f(g x)`);
 val _ = set_fixity "o" (Infixr 800)
-val APP_DEF = def(#(FNAME),#(LINE)) ("APP_DEF",   `$:> x f = f x`);
+val APP_DEF = def(#(FILE),#(LINE)) ("APP_DEF",   `$:> x f = f x`);
 
-val UPDATE_def = def(#(FNAME),#(LINE))("UPDATE_def",
+val UPDATE_def = def(#(FILE),#(LINE))("UPDATE_def",
    `UPDATE a b = \f c. if a = c then b else f c`);
 
 val _ = set_fixity ":>" (Infixl 310);

tools/Holmake/HolLex

@@ -321,8 +321,8 @@ ProofLine = {newline}"Proof"({ws}*"["{optallws}{defn_attribute_list}{optallws}"]
 );
 <INITIAL>"#(LINE)" => (Decl (LinePragma yypos, NONE));
 <INITIAL>"#(LINE="[0-9]+")" => (Decl (LinePragmaWith (yypos, yytext), NONE));
-<INITIAL>"#(FNAME)" => (Decl (FilePragma yypos, NONE));
-<INITIAL>"#(FNAME="[-A-Za-z0-9/$()_.]+")" => (Decl (FilePragmaWith (yypos, yytext), NONE));
+<INITIAL>"#(FILE)" => (Decl (FilePragma yypos, NONE));
+<INITIAL>"#(FILE="[-A-Za-z0-9/$()_.]+")" => (Decl (FilePragmaWith (yypos, yytext), NONE));
 <INITIAL>"\"" => (
   YYBEGIN string;
   case continue() of

tools/Holmake/HolParser.sml

@@ -529,10 +529,10 @@ structure ToSML = struct
           | SOME num => line := (fn (_, pos) => (num - 1, pos)) (!line);
           aux " "; p + size text
         end
-      | FilePragma p => (regular (pos, p); aux (mlquote (!filename)); p + 8)
+      | FilePragma p => (regular (pos, p); aux (mlquote (!filename)); p + 7)
       | FilePragmaWith (p, text) => (
           regular (pos, p);
-          filename := String.substring(text, 8, size text - 9);
+          filename := String.substring(text, 7, size text - 8);
           aux " "; p + size text)
     and doDecls start [] stop = regular (start, stop)
       | doDecls start (d :: ds) stop = doDecls (doDecl false start d) ds stop

tools/Holmake/QFRead.sig

@@ -17,7 +17,7 @@ val streamToReader : bool -> string -> TextIO.instream -> reader
 
    The strings in {input,stream}ToReader allow the specification of the
    filename associated with the stream; the quotation filter will quote
-   this name back to the user with the #(FNAME) directive.
+   this name back to the user with the #(FILE) directive.
 *)
 
 (* In inputFile and fileToReader, the determination is made on whether or

tools/Holmake/QuoteFilter

@@ -266,13 +266,13 @@ ProofLine =
        | SOME i => setlinenum i yyarg;
      (yypos, " "))
 );
-<INITIAL> "#(FNAME)" => (
+<INITIAL> "#(FILE)" => (
   if quotefix then (yypos,yytext)
   else (yypos, "\"" ^ !scriptfilename ^ "\"")
 );
-<INITIAL> "#(FNAME="[-A-Za-z0-9/$()_.]+")" => (
+<INITIAL> "#(FILE="[-A-Za-z0-9/$()_.]+")" => (
   if quotefix then (yypos,yytext)
-  else (scriptfilename := String.substring(yytext,8,size yytext-9);
+  else (scriptfilename := String.substring(yytext,7,size yytext-8);
         (yypos, " "))
 );
 <INITIAL,thmval,TERMINATION_VAL>"(*" => (
@@ -322,7 +322,7 @@ ProofLine =
   (yypos,
    if inscript andalso not quotefix then
      let
-       infix |> 
+       infix |>
        fun extract (s,p) l =
            if List.exists (fn (a,_) => a = s) l then
              (p, List.filter (fn (a,_) => a <> s) l)
@@ -354,7 +354,7 @@ ProofLine =
 (
   if inscript andalso not quotefix then
     let
-      infix |> 
+      infix |>
       val pfx = mlswitch (!mltype_stack) "" "" ");"
       val s0 = String.extract(yytext,0,SOME (size yytext - 1)) (* drop colon *)
       val s = s0 |> Substring.full |> Substring.dropr Char.isSpace
@@ -828,7 +828,7 @@ ProofLine =
 
 <quote,tmquote,tyquote,defnquote,datatypequote,rawquote>"^"{symbol} => ((yypos, (ECHO yyarg yytext)));
 <defnquote0>"^"{symbol} => (
-  (yypos, if quotefix then yytext 
+  (yypos, if quotefix then yytext
           else (inc conjcount; YYBEGIN defnquote; yytext))
 );
 <quote,tmquote,tyquote,defnquote0,defnquote,datatypequote,rawquote>{newline} =>
@@ -857,7 +857,7 @@ ProofLine =
      YYBEGIN INITIAL;
      nextline yyarg (yypos + size yytext);
      if quotefix then yytext
-     else 
+     else
        (if !inddefp then ")" else "") ^ "\"\n] NONE; " ^ magic_bind yyarg ^
        String.concat (List.map (extra_binds (!stem)) (!labelidxs))
     )

tools/Holmake/tests/quote-filter/expected-mosml

@@ -92,4 +92,4 @@ val thmname = boolLib.save_thm("thmname", expression
 val x = 92 + 10;
 val   y = 11
 val s = ""  
-val s' = "foo.sml" (* #(FNAME) *)
+val s' = "foo.sml" (* #(FILE) *)

tools/Holmake/tests/quote-filter/expected-poly

@@ -92,4 +92,4 @@ val thmname = boolLib.save_thm("thmname", expression
 val x = 92 + 10;
 val   y = 11
 val s = ""  
-val s' = "foo.sml" (* #(FNAME) *)
+val s' = "foo.sml" (* #(FILE) *)

tools/Holmake/tests/quote-filter/input

@@ -91,5 +91,5 @@ End
 
 val x = #(LINE) + 10;
 val #(LINE=11) y = #(LINE)
-val s = #(FNAME) #(FNAME=foo.sml)
-val s' = #(FNAME) (* #(FNAME) *)
+val s = #(FILE) #(FILE=foo.sml)
+val s' = #(FILE) (* #(FILE) *)