Login

Create new posts

At least 10 characters

Entities involved:

Preview:

Kotlin

qlbf 的博客真的支持 Kotlin 的高亮吗？

qlbf 的博客真的支持 Kotlin 的高亮吗？

class Abcd<T>(val clazz: Class<T>) {
  fun printGenericParameter() = clazz.canonicalName
  companion object {
    inline operator fun <reified T> invoke() = Abcd(T::class.java)

    @JvmStatic fun Array<String>.main() {
      val abcd = Abcd<LiceInjectionElement>()
      abcd.printGenericParameter().let(::println)
    }
  }
}

Colliot1/3/2018, 1:45:45 PM

fun main(args: Array<String>) {
  val list = object : ArrayList<String>(), Cloneable {
    override fun clone(): Any {
      return super<ArrayList>.clone()
    }
  }
  System.out.println(list)
}

run breaking@ {
  (0..20).forEach continuing@ {
    if (10 <= it) return@breaking
    println(it)
  }
}

infix fun Int.`+`(int: Int) = this * int
fun Array<String>.main() {
  println(1 `+` 10) // 输出 10
  println(1 + 10) // 输出 11
}

这些高亮在 qlbf 的博文里全部有问题。

Reply
Colliot1/3/2018, 1:47:18 PM

我也找不到更好的高亮插件了，我稍微写复杂点它就没法parse了。

Jekyll 能用的高亮插件我记得的有两个，当初研究 Agda 的时候折腾了下，结果全都不支持 Agda 。
Python 写的那个被抛弃了，我现在用的是 Rouge 。

Reply
ice10001/4/2018, 7:10:24 AM

我也找不到更好的高亮插件了，我稍微写复杂点它就没法parse了。

Jekyll 能用的高亮插件我记得的有两个，当初研究 Agda 的时候折腾了下，结果全都不支持 Agda 。
Python 写的那个被抛弃了，我现在用的是 Rouge 。

by ice1000

好吧，知乎的貌似也是个菜鸡……这篇专栏里的高亮也不对。

Reply
Colliot1/4/2018, 7:24:11 AM

让我们来试试高亮 Agda

{-# OPTIONS --without-K --rewriting #-}

open import lib.Basics
open import lib.types.Int
open import lib.types.Pi

module lib.types.Group where

-- 1-approximation of groups without higher coherence conditions.
record GroupStructure {i} (El : Type i) --(El-level : has-level 0 El)
  : Type i where
  constructor group-structure
  field
    ident  : El
    inv    : El → El
    comp   : El → El → El
    unit-l : ∀ a → comp ident a == a
    assoc  : ∀ a b c → comp (comp a b) c == comp a (comp b c)
    inv-l  : ∀ a → (comp (inv a) a) == ident

  ⊙El : Ptd i
  ⊙El = ⊙[ El , ident ]

  private
    infix 80 _⊙_
    _⊙_ = comp

  abstract
    inv-r  : ∀ g → g ⊙ inv g == ident
    inv-r g =
      g ⊙ inv g                           =⟨ ! `_mathjax_internal$ unit-l (g ⊙ inv g) ⟩
      ident ⊙ (g ⊙ inv g)                 =⟨ ! $]^$` inv-l (inv g) |in-ctx _⊙ (g ⊙ inv g) ⟩
      (inv (inv g) ⊙ inv g) ⊙ (g ⊙ inv g) =⟨ assoc (inv (inv g)) (inv g) (g ⊙ inv g) ⟩
      inv (inv g) ⊙ (inv g ⊙ (g ⊙ inv g)) =⟨ ! $ assoc (inv g) g (inv g) |in-ctx inv (inv g) ⊙_ ⟩
      inv (inv g) ⊙ ((inv g ⊙ g) ⊙ inv g) =⟨ inv-l g |in-ctx (λ h → inv (inv g) ⊙ (h ⊙ inv g)) ⟩
      inv (inv g) ⊙ (ident ⊙ inv g)       =⟨ unit-l (inv g) |in-ctx inv (inv g) ⊙_ ⟩
      inv (inv g) ⊙ inv g                 =⟨ inv-l (inv g) ⟩
      ident                               =∎
Reply
Colliot1/4/2018, 7:25:07 AM

让我们来试试高亮 Agda

{-# OPTIONS --without-K --rewriting #-}

open import lib.Basics
open import lib.types.Int
open import lib.types.Pi

module lib.types.Group where

-- 1-approximation of groups without higher coherence conditions.
record GroupStructure {i} (El : Type i) --(El-level : has-level 0 El)
  : Type i where
  constructor group-structure
  field
    ident  : El
    inv    : El → El
    comp   : El → El → El
    unit-l : ∀ a → comp ident a == a
    assoc  : ∀ a b c → comp (comp a b) c == comp a (comp b c)
    inv-l  : ∀ a → (comp (inv a) a) == ident

  ⊙El : Ptd i
  ⊙El = ⊙[ El , ident ]

  private
    infix 80 _⊙_
    _⊙_ = comp

  abstract
    inv-r  : ∀ g → g ⊙ inv g == ident
    inv-r g =
      g ⊙ inv g                           =⟨ ! `_mathjax_internal$ unit-l (g ⊙ inv g) ⟩
      ident ⊙ (g ⊙ inv g)                 =⟨ ! $]^$` inv-l (inv g) |in-ctx _⊙ (g ⊙ inv g) ⟩
      (inv (inv g) ⊙ inv g) ⊙ (g ⊙ inv g) =⟨ assoc (inv (inv g)) (inv g) (g ⊙ inv g) ⟩
      inv (inv g) ⊙ (inv g ⊙ (g ⊙ inv g)) =⟨ ! $ assoc (inv g) g (inv g) |in-ctx inv (inv g) ⊙_ ⟩
      inv (inv g) ⊙ ((inv g ⊙ g) ⊙ inv g) =⟨ inv-l g |in-ctx (λ h → inv (inv g) ⊙ (h ⊙ inv g)) ⟩
      inv (inv g) ⊙ (ident ⊙ inv g)       =⟨ unit-l (inv g) |in-ctx inv (inv g) ⊙_ ⟩
      inv (inv g) ⊙ inv g                 =⟨ inv-l (inv g) ⟩
      ident                               =∎
by Colliot

好吧，不行……这 PrismJS 貌似也是个菜鸡

Reply
Colliot1/4/2018, 7:26:18 AM

很明显你这垃圾也不支持我写的Kotlin代码，你看那些背景是白色的字符，是不是意思是说没过Tokenizer。

Reply
ice10001/10/2018, 11:27:49 AM

很明显你这垃圾也不支持我写的Kotlin代码，你看那些背景是白色的字符，是不是意思是说没过Tokenizer。

by ice1000

不是，支持的，它这个样式就是 operator 带白色背景……

Reply
Colliot1/10/2018, 4:02:56 PM

Preview:

Cancel

Elsewhere

ice1000 replied to TeX 的源码到底在哪里？

就是去掉那两个引号啊，只保留左边的那个竖线和文字的灰色

Colliot replied to 我终于（可能）实现了本站的热更新……

我觉得正确的方式应该是手动给一个重启成功的信号，至少不至于让开头初始化的部分就挂了……不过初始化挂了，和初始化成功但是每次请求都挂，似乎也没多大区别。

Colliot replied to 我终于（可能）实现了本站的热更新……

pm2 的 reload 功能好像不是很稳，重启有错也能重启。或者说这其实是运行时错误，pm2 不把它当成重启失败。

Colliot replied to TeX 的源码到底在哪里？

正确的引用样式是什么？

ice1000 replied to TeX 的源码到底在哪里？

虎哥你这个quote的辣眼睛的两个引号什么时候可以弄掉啊。

ice1000 replied to TeX 的源码到底在哪里？

这么写渲染居然没有出问题。 在格上，Kleene 不动点定理(Kleene's fixed point theorem)的内容是： 如果 (L, sqsubseteq) 是一个完备格，并且函数 f : L to L 是连续的，那么有：<br/>

athit{lfp}(f) = mathit{sup}(K(bot))

Colliot replied to TeX 的源码到底在哪里？

我可能找到了，在这里。Web 语言写的，该怎么让它发挥作用呢？

ice1000 replied to 为什么这里的 MathJax 会闪烁，而 StackExchange 的不会？

肯定啊。双缓冲是个很简单的东西嘛。。。

ice1000 replied to bct水群卖弱控制不住了

你就是头号卖弱犯，踢了

nickname replied to PDF 格式的标准在哪里呢？

ISO 32000-1:2008, Document management -- Portable document format -- Part 1: PDF 1.7 Free to download provided Adobe: http://www.adobe.com/devnet/pdf/pdf_reference.html ISO 32000-2:2017, Document management -- Portable document format -- Part 2: PDF 2.0 Sell for CHF 198 (about ¥1318 Chinese Yuan) from ISO.org: https://www.iso.org/standard/63534.html

Create new posts

At least 10 characters

Entities involved:

Preview: