Created
August 18, 2019 13:03
-
-
Save abenori/b3d09bb02c90dfaa428554714376a602 to your computer and use it in GitHub Desktop.
RIMS用SATySFiファイル
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| % -*- coding: utf-8 -*- | |
| @require: pervasives | |
| @require: gr | |
| @require: list | |
| @require: math | |
| @require: color | |
| @require: option | |
| @require: annot | |
| type config = (| | |
| show-pages : bool; | |
| twoside : bool; | |
| top-space : length; | |
| bottom-space : length; | |
| gutter : length; | |
| fore-edge : length; | |
| paper-size : page; | |
| header-sep : length; | |
| header-height : length; | |
| |) | |
| module RIMS : sig | |
| val default-config : config | |
| val document : 'a -> config ?-> block-text -> document | |
| constraint 'a :: (| | |
| title : inline-text; | |
| author : inline-text; | |
| show-toc : bool; | |
| show-title : bool; | |
| |) | |
| val font-latin-italic : string * float * float | |
| direct \ref : [string] inline-cmd | |
| direct \ref-page : [string] inline-cmd | |
| direct \figure : [inline-text; block-text] inline-cmd | |
| direct +p : [inline-text] block-cmd | |
| direct +pn : [inline-text] block-cmd | |
| direct +abstract : [inline-text] block-cmd | |
| direct +section : [string?; string?; inline-text; block-text] block-cmd | |
| direct +subsection : [string?; string?; inline-text; block-text] block-cmd | |
| direct \emph : [inline-text] inline-cmd | |
| direct \textbf : [inline-text] inline-cmd | |
| direct +definition : [inline-text?; string?; inline-text] block-cmd | |
| direct +theorem : [inline-text?; string?; inline-text] block-cmd | |
| direct +assumption : [inline-text?; string?; inline-text] block-cmd | |
| direct +corollary : [inline-text?; string?; inline-text] block-cmd | |
| direct +lemma : [inline-text?; string?; inline-text] block-cmd | |
| direct +proposition : [inline-text?; string?; inline-text] block-cmd | |
| direct +proof : [inline-text?; inline-text] block-cmd | |
| end = struct | |
| type toc-element = | |
| | TOCElementSection of string * inline-text | |
| | TOCElementSubsection of string * inline-text | |
| let generate-fresh-label = | |
| let-mutable count <- 0 in | |
| (fun () -> ( | |
| let () = count <- !count + 1 in | |
| `generated:` ^ (arabic (!count)) | |
| )) | |
| let no-pads = (0pt, 0pt, 0pt, 0pt) | |
| let-inline \ref key = | |
| let opt = get-cross-reference (key ^ `:num`) in | |
| match opt with | |
| | None -> {?} | |
| | Some(s) -> embed-string s | |
| let-inline \ref-page key = | |
| let opt = get-cross-reference (key ^ `:page`) in | |
| match opt with | |
| | None -> {?} | |
| | Some(s) -> embed-string s | |
| let font-size-normal = 10.5pt | |
| let font-size-title = 16pt | |
| let font-size-author = font-size-normal | |
| let font-size-section = font-size-normal | |
| let font-size-subsection = font-size-normal | |
| let font-size-header = font-size-normal *' 0.9 | |
| let section-top-margin = 20pt | |
| let section-bottom-margin = 12pt | |
| let font-ratio-latin = 1. | |
| let font-ratio-cjk = 0.92 | |
| let baselineskip = (font-size-normal *' font-ratio-cjk) *' 1.7 | |
| let font-latin-roman = (`lmroman` , font-ratio-latin, 0.) | |
| let font-latin-italic = (`lmroman-it`, font-ratio-latin, 0.) | |
| let font-latin-sans = (`lmroman-b` , font-ratio-latin, 0.) | |
| let font-cjk-mincho = (`ipaexm` , font-ratio-cjk , 0.) | |
| let font-cjk-gothic = (`ipaexg` , font-ratio-cjk , 0.) | |
| let set-cjk-font font ctx = | |
| ctx |> set-font HanIdeographic font | |
| |> set-font Kana font | |
| let get-standard-context wid = | |
| get-initial-context wid (command \math) | |
| |> set-dominant-wide-script Kana | |
| |> set-language Kana Japanese | |
| |> set-language HanIdeographic Japanese | |
| |> set-dominant-narrow-script Latin | |
| |> set-language Latin English | |
| |> set-font Kana font-cjk-mincho | |
| |> set-font HanIdeographic font-cjk-mincho | |
| |> set-font Latin font-latin-roman | |
| |> set-math-font `lmodern` | |
| |> set-hyphen-penalty 100 | |
| let-mutable ref-float-boxes <- [] | |
| let height-of-float-boxes pageno = | |
| % let () = display-message `get height` in | |
| (!ref-float-boxes) |> List.fold-left (fun h (pn, bb) -> ( | |
| if pn < pageno then h +' (get-natural-length bb) else h | |
| )) 0pt | |
| let-mutable ref-figure <- 0 | |
| let-inline ctx \figure caption inner = | |
| let () = ref-figure <- !ref-figure + 1 in | |
| let s-num = embed-string (arabic (!ref-figure)) in | |
| let bb-inner = | |
| let d (_, _) _ _ _ = [] in | |
| block-frame-breakable ctx (2pt, 2pt, 2pt, 2pt) (d, d, d, d) (fun ctx -> ( | |
| read-block ctx inner | |
| +++ line-break true true ctx (inline-fil ++ read-inline ctx {図#s-num; #caption;} ++ inline-fil) | |
| )) | |
| in | |
| hook-page-break (fun pbinfo _ -> ( | |
| % let () = display-message (`register` ^ (arabic pbinfo#page-number)) in | |
| ref-float-boxes <- (pbinfo#page-number, bb-inner) :: !ref-float-boxes | |
| )) | |
| let-block ctx +make-title it-title it-author = | |
| let ctx-title = | |
| ctx |> set-font-size font-size-title | |
| |> set-font Latin font-latin-roman | |
| in | |
| let ctx-author = | |
| ctx |> set-font-size font-size-author | |
| |> set-font Latin font-latin-roman | |
| in | |
| let ib-title = read-inline ctx-title it-title in | |
| let ib-author = read-inline ctx-author it-author in | |
| (line-break false false ctx-title (inline-fil ++ ib-title ++ inline-fil)) +++ | |
| (block-skip (font-size-normal *' 0.5)) +++ | |
| (line-break false false ctx-author (inline-fil ++ ib-author ++ inline-fil)) +++ | |
| (block-skip font-size-normal) | |
| let make-section-title ctx = | |
| ctx |> set-font-size font-size-section | |
| |> set-font Latin font-latin-sans | |
| |> set-cjk-font font-cjk-gothic | |
| let make-subsection-title ctx = | |
| ctx |> set-font-size font-size-subsection | |
| |> set-font Latin font-latin-sans | |
| |> set-cjk-font font-cjk-gothic | |
| let-mutable toc-acc-ref <- [] | |
| let-mutable outline-ref <- [] | |
| let get-cross-reference-number label = | |
| match get-cross-reference (label ^ `:num`) with | |
| | None -> `?` | |
| | Some(s) -> s | |
| let get-cross-reference-page label = | |
| match get-cross-reference (label ^ `:page`) with | |
| | None -> `?` | |
| | Some(s) -> s | |
| let default-config = | |
| (| | |
| show-pages = true; | |
| twoside = false; | |
| top-space = 3cm; | |
| bottom-space = 3cm; | |
| gutter = 2.5cm; | |
| fore-edge = 2.5cm; | |
| paper-size = A4Paper; | |
| header-sep = font-size-normal; | |
| header-height = font-size-normal; | |
| |) | |
| let document record ?:configopt inner = | |
| % -- mandatory designations -- | |
| let title = record#title in | |
| let author = record#author in | |
| % -- optional designations -- | |
| let config = Option.from default-config configopt in | |
| % 基本版面 | |
| let paper-size = config#paper-size in | |
| let (paper-width,paper-height) = match paper-size with | |
| | A0Paper -> (841mm,1189mm) | |
| | A1Paper -> (594mm,841mm) | |
| | A2Paper -> (420mm,594mm) | |
| | A3Paper -> (297mm,420mm) | |
| | A4Paper -> (210mm,297mm) | |
| | A5Paper -> (148mm,210mm) | |
| | USLegal -> (8.5inch,14inch) | |
| | USLetter -> (8.5inch,11inch) | |
| | UserDefinedPaper(w,h) -> (w,h) | |
| in | |
| let text-length = paper-width -' (config#gutter +' config#fore-edge) in | |
| let text-height = paper-height -' (config#top-space +' config#bottom-space) in | |
| let header-length = text-length in | |
| let get-x-origin pagenum = | |
| if config#twoside && (pagenum mod 2 == 0) then | |
| config#fore-edge | |
| else | |
| config#gutter | |
| in | |
| let pagecontf pbinfo = | |
| let hgtfb = height-of-float-boxes pbinfo#page-number in | |
| let v = config#top-space in | |
| let h = get-x-origin(pbinfo#page-number) in | |
| % let () = display-message (`hgtfb = ` ^ show-float(hgtfb /' 1pt)) in | |
| (| | |
| text-origin = (h, v +' hgtfb); | |
| text-height = text-height -' hgtfb | |
| |) | |
| in | |
| % -- constants | |
| let thickness = 0.5pt in | |
| let linegap = baselineskip -' (font-size-normal *' font-ratio-cjk) in | |
| let ctx-doc = (get-standard-context text-length) | |
| |> set-font-size font-size-normal | |
| |> set-leading baselineskip | |
| |> set-paragraph-margin linegap linegap | |
| |> set-min-gap-of-lines 1pt | |
| in | |
| % -- title -- | |
| let bb-title = | |
| if record#show-title then | |
| read-block ctx-doc '<+make-title(title)(author);> | |
| else | |
| block-nil | |
| in | |
| % -- main -- | |
| let bb-main = read-block ctx-doc inner in | |
| % -- table of contents -- | |
| let bb-toc = | |
| if not record#show-toc then | |
| block-nil | |
| else | |
| let bb-toc-title = | |
| line-break true false ctx-doc (read-inline (make-section-title ctx-doc) {目次} ++ inline-fil) | |
| in | |
| let bb-toc-main = | |
| (!toc-acc-ref) |> List.reverse |> List.fold-left (fun bbacc tocelem -> ( | |
| match tocelem with | |
| | TOCElementSection(label, title) -> | |
| let it-num = embed-string (get-cross-reference-number label) in | |
| let it-page = embed-string (get-cross-reference-page label) in | |
| bbacc +++ line-break true true ctx-doc | |
| (inline-frame-breakable no-pads (Annot.link-to-location-frame label None) | |
| (read-inline ctx-doc {#it-num;. #title;} ++ inline-fil ++ read-inline ctx-doc it-page)) | |
| | TOCElementSubsection(label, title) -> | |
| let it-num = embed-string (get-cross-reference-number label) in | |
| let it-page = embed-string (get-cross-reference-page label) in | |
| bbacc +++ line-break true true ctx-doc | |
| (inline-skip 20pt ++ (inline-frame-breakable no-pads | |
| (Annot.link-to-location-frame label None) | |
| (read-inline ctx-doc {#it-num;. #title;} ++ inline-fil ++ read-inline ctx-doc it-page))) | |
| )) block-nil | |
| in | |
| bb-toc-title +++ bb-toc-main | |
| in | |
| % -- page settings -- | |
| let pagepartsf pbinfo = | |
| let pageno = pbinfo#page-number in | |
| let header = | |
| let ctx = | |
| get-standard-context header-length | |
| |> set-paragraph-margin 0pt 0pt | |
| |> set-font-size font-size-header | |
| in | |
| let ib-text = | |
| if pageno == 1 then | |
| inline-fil | |
| else | |
| (inline-fil ++ read-inline ctx title ++ inline-fil) | |
| in | |
| % let () = display-message `insert` in | |
| let (bb-float-boxes, acc) = | |
| (!ref-float-boxes) |> List.fold-left (fun (bbacc, acc) elem -> ( | |
| let (pn, bb) = elem in | |
| if pn < pageno then | |
| let bbs = | |
| line-break true true (ctx |> set-paragraph-margin 0pt 12pt) | |
| (inline-fil ++ embed-block-top ctx text-length (fun _ -> bb) ++ inline-fil) | |
| % 'ctx' is a dummy context | |
| in | |
| (bbacc +++ bbs, acc) | |
| else | |
| (bbacc, elem :: acc) | |
| )) (block-nil, []) | |
| in | |
| let () = ref-float-boxes <- acc in | |
| line-break true true ctx ib-text | |
| +++ bb-float-boxes | |
| in | |
| let footer = | |
| if config#show-pages then | |
| let ctx = get-standard-context header-length | |
| |> set-font-size font-size-header | |
| in | |
| let it-pageno = embed-string (arabic pbinfo#page-number) in | |
| line-break true true ctx | |
| (inline-fil ++ (read-inline ctx {#it-pageno;}) ++ inline-fil) | |
| else | |
| block-nil | |
| in | |
| let xorigin = get-x-origin(pbinfo#page-number) in | |
| (| | |
| header-origin = (xorigin,config#top-space -' config#header-sep -' config#header-height); | |
| header-content = header; | |
| footer-origin = (xorigin,paper-height -' config#bottom-space +' config#header-sep +' config#header-height -' baselineskip +' font-size-normal); | |
| footer-content = footer; | |
| |) | |
| in | |
| let doc = page-break paper-size pagecontf pagepartsf (bb-title +++ bb-toc +++ bb-main) in | |
| let () = register-outline (List.reverse !outline-ref) in | |
| doc | |
| let-mutable needs-indentation-ref <- true | |
| let-mutable num-section <- 0 | |
| let-mutable num-subsection <- 0 | |
| let quad-indent ctx = | |
| inline-skip (get-font-size ctx) | |
| let-block ctx +p inner = | |
| let needs-indentation = | |
| if !needs-indentation-ref then true else | |
| let () = needs-indentation-ref <- true in | |
| false | |
| in | |
| let ib-inner = read-inline ctx inner in | |
| let br-parag = | |
| if needs-indentation then | |
| (quad-indent ctx) ++ ib-inner ++ inline-fil | |
| else | |
| ib-inner ++ inline-fil | |
| in | |
| form-paragraph ctx br-parag | |
| let-block ctx +pn inner = | |
| let () = needs-indentation-ref <- true in | |
| let ib-inner = read-inline ctx inner in | |
| form-paragraph ctx (ib-inner ++ inline-fil) | |
| let section-scheme ctx label title outline-title-opt inner = | |
| let ctx-title = make-section-title ctx in | |
| let () = num-section <- !num-section + 1 in | |
| let () = num-subsection <- 0 in | |
| let () = needs-indentation-ref <- true in | |
| let s-num = arabic (!num-section) in | |
| let () = register-cross-reference (label ^ `:num`) s-num in | |
| let () = toc-acc-ref <- (TOCElementSection(label, title)) :: !toc-acc-ref in | |
| let ib-num = | |
| read-inline ctx-title (embed-string (s-num)) | |
| ++ hook-page-break (fun pbinfo _ -> register-cross-reference (label ^ `:page`) (arabic pbinfo#page-number)) | |
| in | |
| let ib-title = read-inline ctx-title title in | |
| let outline-title = Option.from (extract-string ib-title) outline-title-opt in | |
| let () = outline-ref <- (0, s-num ^ `. `# ^ outline-title, label, false) :: !outline-ref in | |
| let bb-title = | |
| block-frame-breakable ctx no-pads (Annot.register-location-frame label) (fun ctx -> ( | |
| (line-break true false (ctx |> set-paragraph-margin section-top-margin section-bottom-margin) | |
| (ib-num ++ (inline-skip font-size-normal) ++ ib-title ++ (inline-fil))))) | |
| in | |
| let bb-inner = read-block ctx inner in | |
| bb-title +++ bb-inner | |
| let subsection-scheme ctx label title outline-title-opt inner = | |
| let () = num-subsection <- !num-subsection + 1 in | |
| let () = needs-indentation-ref <- false in | |
| let s-num = arabic (!num-section) ^ `.` ^ arabic (!num-subsection) in | |
| let () = register-cross-reference (label ^ `:num`) s-num in | |
| let () = toc-acc-ref <- (TOCElementSubsection(label, title)) :: !toc-acc-ref in | |
| let ctx-title = make-subsection-title ctx in | |
| let ib-num = | |
| read-inline ctx-title (embed-string (s-num ^ `.`)) | |
| ++ hook-page-break (fun pbinfo _ -> register-cross-reference (label ^ `:page`) (arabic pbinfo#page-number)) | |
| in | |
| let ib-title = read-inline ctx-title title in | |
| let outline-title = Option.from (extract-string ib-title) outline-title-opt in | |
| let () = outline-ref <- (1, s-num ^ `. `# ^ outline-title, label, false) :: !outline-ref in | |
| let bb-title = | |
| line-break true false (ctx |> set-paragraph-margin section-top-margin section-bottom-margin) | |
| (inline-frame-breakable no-pads (Annot.register-location-frame label) | |
| (ib-num ++ (inline-skip 10pt) ++ ib-title ++ (inline-fil))) | |
| in | |
| let bb-inner = read-block ctx inner in | |
| bb-title +++ bb-inner | |
| let-block ctx +section ?:labelopt ?:outline-title-opt title inner = | |
| let label = | |
| match labelopt with | |
| | None -> generate-fresh-label () | |
| | Some(label) -> label | |
| in | |
| section-scheme ctx label title outline-title-opt inner | |
| let-block ctx +subsection ?:labelopt ?:outline-title-opt title inner = | |
| let label = | |
| match labelopt with | |
| | None -> generate-fresh-label () | |
| | Some(label) -> label | |
| in | |
| subsection-scheme ctx label title outline-title-opt inner | |
| let-inline ctx \emph inner = | |
| let ctx-emph = | |
| ctx |> set-font Latin font-latin-italic | |
| |> set-cjk-font font-cjk-gothic | |
| in | |
| read-inline ctx-emph inner | |
| let-inline ctx \textbf inner = | |
| let ctx-textbf = | |
| ctx |> set-font HanIdeographic font-cjk-gothic | |
| |> set-font Kana font-cjk-gothic | |
| |> set-font Latin font-latin-sans | |
| in | |
| read-inline ctx-textbf inner | |
| let theorem-beforeafter-space = baselineskip *' 0.5 | |
| let-mutable definition-counter <- 0 | |
| let theorem-protytype theorem-name counter ctx ?:title ?:label inner = | |
| let font-size = get-font-size ctx in | |
| let () = counter <- !counter + 1 in | |
| let subtitle = match title with | |
| | None -> inline-nil | |
| | Some(s) -> (read-inline ctx (embed-string(`（`))) ++ (read-inline ctx s) ++ (read-inline ctx (embed-string(`）`))) | |
| in | |
| let () = match label with | |
| | None -> () | |
| | Some(s) -> register-cross-reference (s ^ `:num`) (arabic !counter) | |
| in | |
| let subtitle-text = embed-string(theorem-name ^ (arabic !counter)) in | |
| let ctx-gothic = | |
| ctx |> set-font HanIdeographic font-cjk-gothic | |
| |> set-font Kana font-cjk-gothic | |
| |> set-font Latin font-latin-sans | |
| in | |
| let subtitle-box = (read-inline ctx-gothic {#subtitle-text;}) ++ subtitle ++ inline-skip (font-size) in | |
| let inner-box = read-inline ctx inner in | |
| let margin = theorem-beforeafter-space +' baselineskip -' font-size-normal in | |
| let theorem-ctx = ctx | |
| |> set-paragraph-margin margin margin | |
| in | |
| line-break true true theorem-ctx (subtitle-box ++ inner-box ++ inline-fil) | |
| let-block ctx +definition = theorem-protytype `定義` definition-counter ctx | |
| let-block ctx +theorem = theorem-protytype `定理` definition-counter ctx | |
| let-block ctx +lemma = theorem-protytype `補題` definition-counter ctx | |
| let-block ctx +assumption = theorem-protytype `仮定` definition-counter ctx | |
| let-block ctx +corollary = theorem-protytype `系` definition-counter ctx | |
| let-block ctx +proposition = theorem-protytype `命題` definition-counter ctx | |
| let qedsymbol ctx = | |
| let font-size = get-font-size ctx in | |
| let w = font-size *' 0.5 in | |
| let d = font-size *'0.12 in | |
| let h = font-size *'0.88 in | |
| let thickness = 0.5pt in | |
| let color = Color.black in | |
| inline-graphics w h d (fun (x,y) -> | |
| [ | |
| stroke thickness color (Gr.rectangle (x,y -' d) (x +' w,y +' h)); | |
| ] | |
| ) | |
| let-block ctx +proof ?:title inner = | |
| let font-size = get-font-size ctx in | |
| let prooftitle = match title with | |
| | None -> {証明} | |
| | Some(s) -> s | |
| in | |
| let ctx-gothic = | |
| ctx |> set-font HanIdeographic font-cjk-gothic | |
| |> set-font Kana font-cjk-gothic | |
| |> set-font Latin font-latin-sans | |
| in | |
| let ib-inner = (read-inline ctx-gothic {#prooftitle;}) ++ (inline-skip font-size) ++ (read-inline ctx inner) ++ inline-fil ++ (qedsymbol ctx) in | |
| let margin = theorem-beforeafter-space +' baselineskip -' font-size-normal in | |
| let theorem-ctx = ctx | |
| |> set-paragraph-margin margin margin | |
| in | |
| line-break true true theorem-ctx ib-inner | |
| let-block ctx +abstract inner = | |
| let ctx-gothic = | |
| ctx |> set-font HanIdeographic font-cjk-gothic | |
| |> set-font Kana font-cjk-gothic | |
| |> set-font Latin font-latin-sans | |
| in | |
| let indent = inline-skip (get-font-size ctx) in | |
| (line-break true false ctx (inline-fil ++ (read-inline ctx-gothic {概要}) ++ inline-fil)) +++ | |
| (line-break false true ctx (indent ++ (read-inline ctx inner) ++ inline-fil)) +++ | |
| (block-skip 10pt) | |
| end | |
| let document = RIMS.document | |
| % ad-hoc |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment